blob: 6599180a9449b10d44bb3d9d26788af9ea980544 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
-*- mode:outline -*-
* Coq Proof General Bugs
See also ../BUGS for generic bugs.
** Multiple file handling and auto-compilation is incomplete
** C-c C-a C-i on long intro lines breaks line the wrong way.
** 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.
** Others not mentioned...
Please report further issues at http://proofgeneral.inf.ed.ac.uk/trac
|
