Custom Query (361 matches)

Hi,

The following code is rejected by Coq, since [x] is already defined in the second line, but proofgeneral "validates" it (it goes through, so that one has to be really careful to notice the warning in the "coq output" buffer - this can be quite errorprone since Coq keeps the old definition).

<< Definition x := 3. Definition x := 5.

Damien

Here is another piece of Coq code that doesn't parse anymore:

Record a : Type := make_a { aa : nat }.

Hi,

the commit ​http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/d3cf65e2d4e4 brakes parsing in Coq. Try

Require Export Coq.Lists.List.
Notation "[ ]" := nil : list_scope.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.

Bye,

Hendrik