blob: d4df41c388bb6ed10f30c7c33dae15bcddc1ca75 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
-*- mode:outline -*-
* Coq Proof General Bugs
See also ../BUGS for generic bugs.
** X-Symbol does not work on GNU Emacs.
Please don't even try it, it will mess up your Emacs.
** With new syntax in Coq 7, comments at end of files cannot be processed.
Leads to annoying retract/process questions when switching buffers.
Workaround: don't use a comment as the last line of the buffer, for now.
** coqtags doesn't find all declarations.
It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x
but not y. [The same problem exists for legotags] Workaround: don't
rely too much on the etags mechanism.
** User defined tactics cannot be retracted.
Workaround: you may need to retract to the beginning of the proof.
** Coq Proof General does not know about Coq's Section mechanism.
** Surely others that aren't mentioned here...
Please report them to proofgen@dcs.ed.ac.uk.
|
