From 72ea2bfb9bd301c8b168e0c5b8bdab7bf4d3461c Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 29 Sep 2000 13:29:49 +0000
Subject: 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).

---
 coq/coq.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index 2b8495a2..eae46efd 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.")
-- 
cgit v1.2.3