| Age | Commit message (Collapse) | Author |
|---|
|
|
|
coq-find-and-forget.
|
|
new "Back n." command of coq to make the syncronization better. Seems
to work, need to test.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
this variable more trustable with (concat coq-prog-name "-v").
|
|
|
|
ended by ".eof"
|
|
|
|
coq-version-is-V7
|
|
'goalsave -> 'proof
|
|
|
|
|
|
|
|
allow both V6 and V7 for a while. Theoretically, incompatibilities
will not be numerous.
|
|
|
|
|
|
|
|
|
|
uses Reset Initial which doesn't reset the Implicit Arguments flag to
Off (this is the bug), I added the good command to the coq reset
command, this has to be backtracked when V7 will be done (the bug is
already corrected in V7).
|
|
|
|
|
|
coq/x-symbol-coq.el
|
|
coq/coq-syntax.el and coq/coq.el.
|
|
completely definitions and theorems, but proof script are hidden (but
can be blindly sent to the prover). Seems to work correctly.
|
|
one problem remains: a word ending with phi will be encoded.
|
|
|
|
|
|
|
|
|
|
|
|
commented out
|
|
|
|
|
|
|
|
|
|
|
|
RPM, where its fixed.
|
|
|
|
for other provers (already done ?).
|
|
|
|
|
|
|
|
|
|
|
