diff options
| author | Pierre Courtieu | 2000-09-29 13:29:49 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2000-09-29 13:29:49 +0000 |
| commit | 72ea2bfb9bd301c8b168e0c5b8bdab7bf4d3461c (patch) | |
| tree | 1a66fdf516f96d5236cc71e389c7cbdddf86ed74 | |
| parent | 63000d541743e839c62be74af1158f241124ba42 (diff) | |
A little work around for the bug of Coq concerning the restart that
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).
| -rw-r--r-- | coq/coq.el | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -67,8 +67,11 @@ (format "Set Undo %s." coq-default-undo-limit)) ;; Command to reset the Coq Proof Assistant +;; Pierre: added Impl... because of a bug of Coq until V6.3 +;; (included). The bug is already fixed in the next version (V7). So +;; we will backtrack this someday. (defconst coq-shell-restart-cmd - "Reset Initial.") + "Reset Initial.\n Implicit Arguments Off.") (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ") "*The prompt pattern for the inferior shell running coq.") |