| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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 ?).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-shell-filename-escapes, and always apply for filename substn.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-shell-eager-annotation-start-length.
|
|
|
|
|
|
|
