Small fixes from Stefan Monnier.

3 files changed, 34 insertions, 29 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 3265b501..28f48ffd 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -54,7 +54,7 @@ ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
      (coq-version-is-V8 (setq coq-version-is-V8-0 nil coq-version-is-V8-1 t)
                         (message v80))
      (t;; otherwise do coqtop -v and see which version we have
-      (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
+      (let* ((str (shell-command-to-string (concat "cd ~; " coq-prog-name " -v")))
              ;; this match sets match-string below
              (ver (string-match "version v?\\([.0-9]*\\)" str)))
         (message str)
@@ -127,7 +127,7 @@ so for the following reasons:
      ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t)
      ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t)
      ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite")
-     ("cases" "c" "cases " t "cases")
+     ("case" "c" "case " t "case")
      ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv")
      ("change in" "chi" "change # in #" t)
      ("change with in" "chwi" "change # with # in #" t)
@@ -144,10 +144,10 @@ so for the following reasons:
      ("contradiction" "contr" "contradiction" t "contradiction")
      ("cut" "cut" "cut" t "cut")
      ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite")
-     ("decide equality" "deg" "decide equality" t "decide\\-+equality")
+     ("decide equality" "deg" "decide equality" t "decide\\s-+equality")
      ("decompose" "dec" "decompose [#] #" t "decompose")
      ("decompose record" "decr" "decompose record #" t "decompose\\s-+record")
-     ("decompose sum" "decs" "decompose sum #" t "decompose\\-+sum")
+     ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum")
      ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion")
      ("dependent inversion with" "depinvw" "dependent inversion # with #" t)
      ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear")
@@ -754,7 +754,7 @@ Used by `coq-goal-command-p'"
   "Punctuation Symbols used by Coq.")
 
 ;; ----- regular expressions
-(defvar coq-error-regexp "^\\(Error[:]\\|Discarding pattern\\|Syntax error[:]\\|System Error[:]\\|User Error[:]\\|User error[:]\\|Anomaly[:.]\\|Toplevel input[,]\\)"
+(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
   "A regexp indicating that the Coq process has identified an error.")
 
 (defvar coq-id proof-id)
@@ -798,24 +798,24 @@ Used by `coq-goal-command-p'"
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-save)))
 (defconst coq-save-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-save-strict)
-	  "\\)\\s-+\\(" coq-id "\\)\\s-*\."))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
 
 (defconst coq-goal-command-regexp
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal)))
 
 (defconst coq-goal-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-goal)
-	  "\\)\\s-+\\(" coq-id "\\)\\s-*[:]?"))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
           ;; Papageno : ce serait plus propre d'omettre le `:'
           ;; uniquement pour Correctness
           ;; et pour Definition f [x,y:nat] := body
 (defconst coq-decl-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
-	  "\\)\\s-+\\(" coq-ids "\\)\\s-*[:]"))
+	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
 
 (defconst coq-defn-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-defn)
-          "\\)\\s-+\\(" coq-id "\\)\\s-*\\S-"))
+          "\\)\\s-+\\(" coq-id "\\)"))
 
 
 ;;; 'with' is used in tactics too... and ":=" can appear too!! But only
diff --git a/coq/coq.el b/coq/coq.el
index 04be03a1..da249d52 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -15,7 +15,6 @@
 ;; 
 
 (require 'proof)
-(require 'holes-load) ; in lib directory
 (require 'local-vars-list) ; in lib directory
 (require 'coq-local-vars) ; in coq directory
 ;; coq-syntaxe is required below
@@ -140,13 +139,15 @@ controling coq prompt. Only for coq >= 8.1 (and 8.1 beta)")
 
 
 ;; ----- outline
-
+;; FIXME, deal with interacive "Definition"
 (defvar coq-outline-regexp
-  (concat "(\\*\\|" (proof-ids-to-regexp 
+;;  (concat "(\\*\\|" 
+  (concat "[ ]*" (regexp-opt 
 	   '(
-"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Import" "Hint" "Hints" "Hypothesis" "Correctness" "Module" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint" "Save" "Qed" "Defined" "End" "Coercion"))))
+             "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" "Definition" "Lemm" "Theo" "Fact" "Rema" "Mutu" "Fixp") t)))
+;)
 
-(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n")
+(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.[ \t\n]\\|:=")
 
 (defvar coq-shell-outline-regexp coq-goal-regexp)
 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
@@ -648,7 +649,7 @@ happen since one of them is necessarily set to t in coq-syntax.el."
              (buffer-substring-no-properties (region-beginning) (region-end))
            (thing-at-point 'word)))))
     (read-string 
-     (if guess (concat s " (" guess "): ") (concat s " : "))
+     (if guess (concat s " (default " guess "): ") (concat s " : "))
      nil 'proof-minibuffer-history guess)))
 
 
@@ -673,25 +674,25 @@ This is specific to `coq-mode'."
 
 (defun coq-SearchRewrite ()
   (interactive)
-  (coq-ask-do "Search Rewrite :" "Search Rewrite" nil))
+  (coq-ask-do "Search Rewrite" "Search Rewrite" nil))
 
 (defun coq-SearchAbout ()
   (interactive)
-  (coq-ask-do "Search About :" "Search About" nil))
+  (coq-ask-do "Search About" "Search About" nil))
 
 (defun coq-Print () "Ask for an ident and print the corresponding term."
   (interactive)
-  (coq-ask-do "Print:" "Print"))
+  (coq-ask-do "Print" "Print"))
 
 (defun coq-About () "Ask for an ident and print information on it."
   (interactive)
-  (coq-ask-do "About:" "About"))
+  (coq-ask-do "About" "About"))
 
 (defun coq-LocateConstant ()
   "Locate a constant.
 This is specific to `coq-mode'."
   (interactive)
-  (coq-ask-do "Locate :" "Locate"))
+  (coq-ask-do "Locate" "Locate"))
 
 (defun coq-LocateLibrary ()
   "Locate a constant.
@@ -725,7 +726,7 @@ This is specific to `coq-mode'."
 (defun coq-Print-implicit ()
   "Ask for an ident and print the corresponding term."
   (interactive)
-  (coq-ask-do "Print Implicit: " "Print Implicit"))
+  (coq-ask-do "Print Implicit " "Print Implicit"))
 
 (defun coq-Check ()
   "Ask for a term and print its type."
diff --git a/coq/ex-module.v b/coq/ex-module.v
index 413a4966..e6e3511f 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -1,4 +1,4 @@
-
+(*  *)
 Module Type O1.
   Parameter A:Set.
   Parameter B:Set.
@@ -24,18 +24,22 @@ End R4.
 
 
 Module M.
+
   Module Type SIG.
     Parameter T:Set.
     Parameter x:T.
   End SIG.
+
   Module Type SIG'.
     Parameter T:Set.
     Parameter x:T.
   End SIG'.
+
   Lemma toto : O=O.
     Definition t:=nat.
     trivial.
   Save.
+
   Module N:SIG.
     Definition T:=nat.
     Definition x:=O.
@@ -71,16 +75,16 @@ Module Type N'.
     Declare Module K:N.SIG.
   End M'.
 (*   Declare Module N''. *)
-    Definition T:=nat.
-    Definition x:=O.
+  Definition T:=nat.
+  Definition x:=O.
 (*   End N''. *)
   
   Declare Module N':M.SIG. (* no interactive def started *)
   Declare Module N''' :M.SIG. (* no interactive def started *)
 End N'.
 
-    
-    
+
+
 Lemma titi : O=O.
   trivial.
   Module Type K:=N'.
@@ -88,9 +92,9 @@ Lemma titi : O=O.
 Save.
 
 	 (* Here is a bug of Coq: *)
-    
+
 Lemma bar:O=O.
   Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
-  End L. (* fails --> if we go back to Module Type: unsync *)
-  Module I.
+End L. (* fails --> if we go back to Module Type: unsync *)
+Module I.
 End I.