blob: 68cca029723501952b1d33cbcbe1e6f3df0ef415 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
In coq different modules may contain definition with the same
name, because for coq they have different "absolute names" because
they are in different modules.
To provoke an error inside ProofGeneral on correct coq input,
do the following:
- Visit a.v and script the initial comment.
- Set proof-no-fully-processed-buffer to nil.
- assert buffer a.v completely
- switch to b.v
- scripting "Definition a" in b.v will give the error "a already
exists"
Now retract a.v, set proof-no-fully-processed-buffer to t and try
again.
To see that the example is indeed valid, script c.v. (For c.v you
either have to switch coq-recompile-before-require to t or you
have to compile modules a and b yourself with "coqc a" and "coqc b".)
|
