coq

coq copied to clipboard

Syntactic validity of .v files is platform-dependent (0x1a errors on Windows)

2

#### Description of the problem We've been trying to get bedrock2 to build on Windows for inclusion in Coq Platform: https://github.com/mit-plv/bedrock2/issues/273 https://github.com/mit-plv/bedrock2/pull/272 https://github.com/mit-plv/bedrock2/issues/268. It appears that using the byte `0x1a`...

andres-erbsen

ExtrOCamlInt63 contains an upper-case C in its name

10

#### Description of the problem Every other module in that family starts with `ExtrOcaml` instead. This is quite confusing. #### Coq Version master (8.10)

Lysxia

This is not a bug report, just to tell you thank you for the improvement on the efficiency (-14%)! Results with Coq 8.15: ``` 18:51 ~/src/color (master) l log-8.15.0 generate...

fblanqui

SkySkimmer

Namegen.next_ident_away_in_goal: don't avoid names of nonlocal refs

24

Fix #3523 Overlays: - https://github.com/mit-pdos/argosy/pull/4 - https://github.com/fblanqui/color/pull/36 - https://github.com/DeepSpec/sfdev/pull/401 - https://github.com/PrincetonUniversity/VST/pull/528 - https://github.com/MetaCoq/metacoq/pull/603 - TODO

SkySkimmer

Suggestion for minor extension of coq/theories/Logic/FinFun.v: Listing l -> decidable_eq A

6

#### Description of the suggestion I would like to suggest to add one/some of the following lemmata to `coq/theories/Logic/FinFun.v`: ``` Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A....

bodoai

XML protocol state machine documentation link is broken.

2

This link is broken in the [XML protocol docs:](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md): https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md Documenting the state machine that handles the XML protocol. What I really want is to know more about how to...

enjoysmath

Ltac2 library: list and array fold functions don't match OCaml

5

I just found that I well and thoroughly messed up the parameter order of the list and array fold functions back then. I took the OCaml headers as blue print...

MSoegtropIMC

Not_found anomaly via Equations funelim

12

#### Description of the problem The following self-contained code using Equations yields either an incomprehensible error (`Variable k should be bound to a tactic.`) or a plain anomaly (`Anomaly "Uncaught...

palmskog

Ltac2 should provide datatypes for hash sets and hash maps

3

#### Description of the problem I'd like to have hash maps and hash sets where where keys (for map) / values (for sets) are the following types: - `ident` -...

JasonGross