aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/BUGS
blob: 1cf1027bfdfafe186555837bd2361e81fdac5c1c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
-*- mode:outline -*-

* Coq Proof General Bugs

See also ../BUGS for generic bugs.

** 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.

** With Coq 7, multiple file handling and auto-compilation is buggy

** Surely others that aren't mentioned here...
  
Please report them to da+pg-bugs@inf.ed.ac.uk