Deleted compatibility for coq v6 and v7 + new backtracking system. For

now it can be triggered only by using coq-version-is-v8-1.

3 files changed, 372 insertions, 706 deletions

diff --git a/coq/coq-abbrev-V7.el b/coq/coq-abbrev-V7.el
deleted file mode 100644
index 225df006..00000000
--- a/coq/coq-abbrev-V7.el
+++ /dev/null
@@ -1,261 +0,0 @@
-;; default abbrev table
-; This is for coq V7, you should test coq version before loading
-
-;#s are replaced by holes by holes-abbrev-complete
-(if (boundp 'holes-abbrev-complete)
-	 ()
-  (define-abbrev-table 'coq-mode-abbrev-table
-	 '(
-		("a" "Auto" holes-abbrev-complete 4)
-		("ar" "Autorewrite [@{db,db...}] using @{tac}" holes-abbrev-complete 1)
-		("ab" "Absurd " holes-abbrev-complete 0)
-		("abs" "Absurd " holes-abbrev-complete 0)
-		("ap" "Apply " holes-abbrev-complete 16)
-		("as" "Assumption" holes-abbrev-complete 4)
-		("au" "Auto" holes-abbrev-complete 1)
-		("aw" "Auto with " holes-abbrev-complete 1)
-		("awa" "Auto with arith" holes-abbrev-complete 4)
-		("ch" "Change " holes-abbrev-complete 1)
-		("chi" "Change # in #" holes-abbrev-complete 1)
-		("chwi" "Change # with # in #" holes-abbrev-complete 1)
-		("con" "Constructor" holes-abbrev-complete 3)
-		("dec" "Decompose [#] @{hyp}" holes-abbrev-complete 3)
-		("def" "Definition #:# := #." holes-abbrev-complete 5)
-		("def1" "Definition # [# : #] :# := #." holes-abbrev-complete 5)
-		("deg" "Decide Equality" holes-abbrev-complete 3)
-		("des" "Destruct " holes-abbrev-complete 0)
-		("desu" "Destruct # using #" holes-abbrev-complete 0)
-		("desa" "Destruct # as #" holes-abbrev-complete 0)
-		("dis" "Discriminate" holes-abbrev-complete 0)
-		("dm" "Declare Module # : # := #." holes-abbrev-complete 0)
-		("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0)
-		("dmi" "Declare Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
-		("dmi2" "Declare Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
-		("e" "Elim #" holes-abbrev-complete 1)
-		("ea" "Eauto" holes-abbrev-complete 0)
-		("eap" "Eapply #" holes-abbrev-complete 0)
-		("eaw" "Eauto with @{db}" holes-abbrev-complete 0)
-		("eawa" "Eauto with arith" holes-abbrev-complete 0)
-		("el" "Elim #" holes-abbrev-complete 0)
-		("elu" "Elim # using #" holes-abbrev-complete 0)
-		("ex" "Exists #" holes-abbrev-complete 0)
-		("f" "[#:#]#" holes-abbrev-complete 0)
-		("fix" "Fixpoint # [#:#] : # :=\n#." holes-abbrev-complete 3)
-		("fo" "(#:#)#" holes-abbrev-complete 0)
-		("fsto" "Firstorder" holes-abbrev-complete 0)
-		("g" "Generalize #" holes-abbrev-complete 0)
-		("ge" "Generalize #" holes-abbrev-complete 0)
-		("gen" "Generalize #" holes-abbrev-complete 0)
-		("hc" "Hints Constructors # : #." holes-abbrev-complete 0)
-		("he" "Hint # : @{db} := Extern @{cost} (@{pat}) (@{tac})." holes-abbrev-complete 0)
-		("hi" "Hints Immediate # : @{db}." holes-abbrev-complete 0)
-		("hr" "Hints Resolve # : @{db}." holes-abbrev-complete 0)
-		("hrw" "Hint Rewrite -> [@{t1 t2...}] in @{db} using @{tac}." holes-abbrev-complete 0)
-		("hs" "Hints # : #." holes-abbrev-complete 0)
-		("hu" "Hints Unfold # : #." holes-abbrev-complete 0)
-		("i" "Intro " holes-abbrev-complete 10)
-		("if" "if # then # else #" holes-abbrev-complete 1)
-		("in" "Intro" holes-abbrev-complete 1)
-		("ind" "Induction #" holes-abbrev-complete 2)
-		("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
-		("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
-		("inj" "Injection #" holes-abbrev-complete 2)
-		("inv" "Inversion #" holes-abbrev-complete 9)
-		("intu" "Intuition #" holes-abbrev-complete 9)
-		("is" "Intros #" holes-abbrev-complete 11)
-		("ite" "if # then # else #" holes-abbrev-complete 1)
-		("l" "Lemma # : #." holes-abbrev-complete 4)
-		("li" "Let # := # in #" holes-abbrev-complete 1)
-		("c" "Cases # of\n| # => #\nend" holes-abbrev-complete 1)
-		("c2" "Cases # of\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("c3" "Cases # of\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("c4" "Cases # of\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("c5" "Cases # of\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
-		("mt" "Module Type # := #." holes-abbrev-complete 0)
-		("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0)
-		("mo" "Module # : # := #." holes-abbrev-complete 0)
-		("mo2" "Module # <: # := #." holes-abbrev-complete 0)
-		("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
-		("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
-		("o" "Omega" holes-abbrev-complete 0)
-		("om" "Omega" holes-abbrev-complete 0)
-		("p" "Print #" holes-abbrev-complete 3)
-		("po" "Pose ( # := # )" nil 0)
-		("pr" "Print #" holes-abbrev-complete 2)
-		("rep" "Replace # with #" holes-abbrev-complete 19)
-		("r" "Rewrite #" holes-abbrev-complete 19)
-		("r<" "Rewrite <- #" holes-abbrev-complete 0)
-		("rl" "Rewrite <- #" holes-abbrev-complete 0)
-		("refl" "Reflexivity #" holes-abbrev-complete 0)
-		("ri" "Rewrite # in #" holes-abbrev-complete 19)
-		("ril" "Rewrite <- # in #" holes-abbrev-complete 0)
-		("ri<" "Rewrite <- # in #" holes-abbrev-complete 0)
-		("re" "Rewrite #" holes-abbrev-complete 0)
-		("re<" "Rewrite <- #" holes-abbrev-complete 0)
-		("ring" "Ring #" holes-abbrev-complete 19)
-		("s" "Simpl" holes-abbrev-complete 23)
-		("su" "Subst #" holes-abbrev-complete 23)
-		("sc" "Scheme @{name} := Induction for # Sort #." nil 0)
-		("si" "Simpl" holes-abbrev-complete 0)
-		("sp" "Split" holes-abbrev-complete 1)
-		("sy" "Symmetry" holes-abbrev-complete 0)
-		("sym" "Symmetry" holes-abbrev-complete 0)
-		("t" "Trivial" holes-abbrev-complete 1)
-		("tr" "Trivial" holes-abbrev-complete 1)
-		("trans" "Transitivity #" holes-abbrev-complete 1)
-		("ta" "Tauto" holes-abbrev-complete 1)
-		("u" "Unfold #" holes-abbrev-complete 1)
-		("un" "Unfold #" holes-abbrev-complete 7)
-		("v" "Variable # : #." holes-abbrev-complete 7)
-		("vs" "Variables # : #." holes-abbrev-complete 7)
-		)
-	 )
-  )
-
-
-(defpgdefault menu-entries
-  '(
-    ("Insert Command" 
-      "COMMAND               ABBREVIATION"
-     ["Definition            def<C-BS>" (insert-and-expand "def") t]
-     ["Fixpoint              fix<C-BS>" (insert-and-expand "fix") t]
-     ["Lemma                 l<C-BS>" (insert-and-expand "l") t]
-     ""
-     ["Inductive             indv<C-BS>" (insert-and-expand "indv") t]
-     ["Inductive1            indv1<C-BS>" (insert-and-expand "indv1") t]
-     ["Inductive2             indv2<C-BS>" (insert-and-expand "indv2") t]
-     ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
-     ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
-     ""
-     ["Section..." coq-insert-section t]
-     ""
-     ("Modules"
-      "COMMAND               ABBREVIATION"
-      ["Module (interactive)... " coq-insert-module t]
-      ["Module                mo<C-BS>" (insert-and-expand "mo") t]
-      ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
-;      ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
-;      ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
-      ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
-;      ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
-;      ""
-      ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
-      ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
-;      ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
-;      ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
-      )
-     ("Hints"
-      "COMMAND               ABBREVIATION"
-      ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
-      ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
-      ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
-      ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
-      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
-     )
-     ("Schemes"
-      "COMMAND               ABBREVIATION"
-      ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
-      )
-     )
-
-    ("Insert term" 
-     "FORM           ABBREVIATION"
-     ["forall        fo<C-BS>"  (insert-and-expand "fo") t]
-     ""
-     ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
-     ""
-     ["let in        li<C-BS>"  (insert-and-expand "li") t]
-     ""
-     ["Cases         c<C-BS>"  (insert-and-expand "c") t]
-     ["Cases2        c2<C-BS>"  (insert-and-expand "c2") t]
-     ["Cases3        c3<C-BS>"  (insert-and-expand "c3") t]
-     ["Cases4        c4<C-BS>"  (insert-and-expand "c4") t]
-     )
-
-    ("Insert tactic (a-f)" 
-     "TACTIC           ABBREVIATION"
-     ["Absurd                 abs<C-BS>"  (insert-and-expand "abs") t]
-     ["Assumption              as<C-BS>"  (insert-and-expand "as") t]
-     ["Assert                 ass<C-BS>"  (insert-and-expand "ass") t]
-     ["Auto                     a<C-BS>"  (insert-and-expand "a") t]
-     ["Auto with               aw<C-BS>"  (insert-and-expand "aw") t]
-     ["Auto with arith        awa<C-BS>"  (insert-and-expand "awa") t]
-     ["Autorewrite             ar<C-BS>"  (insert-and-expand "ar") t]
-     ["Cases                    c<C-BS>"  (insert-and-expand "c") t]
-     ["Change                  ch<C-BS>"  (insert-and-expand "ch") t]
-     ["Change in              chi<C-BS>"  (insert-and-expand "chi") t]
-     ["Change with in        chwi<C-BS>"  (insert-and-expand "chwi") t]
-     ["Constructor            con<C-BS>"  (insert-and-expand "con") t]
-     ["Congruence            cong<C-BS>"  (insert-and-expand "cong") t]
-     ["Decompose              dec<C-BS>"  (insert-and-expand "dec") t]
-     ["Decide Equality        deg<C-BS>"  (insert-and-expand "deg") t]
-     ["Destruct               des<C-BS>"  (insert-and-expand "des") t]
-     ["Destruct using        desu<C-BS>"  (insert-and-expand "desu") t]
-     ["Destruct as           desa<C-BS>"  (insert-and-expand "desa") t]
-     ["Discriminate           dis<C-BS>"  (insert-and-expand "dis") t]
-     ["Eauto                   ea<C-BS>"  (insert-and-expand "ea") t]
-     ["Eauto with             eaw<C-BS>"  (insert-and-expand "dec") t]
-     ["Elim                     e<C-BS>"  (insert-and-expand "e") t]
-     ["Elim using             elu<C-BS>"  (insert-and-expand "elu") t]
-     ["Exists                  ex<C-BS>"  (insert-and-expand "ex") t]
-     ["Field                  fld<C-BS>"  (insert-and-expand "fld") t]
-     ["Firstorder            fsto<C-BS>"  (insert-and-expand "fsto") t]
-     ["Fourier                fou<C-BS>"  (insert-and-expand "fou") t]
-     )
-
-    ("Insert tactic (g-z)" 
-     "TACTIC           ABBREVIATION"
-     ["Generalize             g<C-BS>"  (insert-and-expand "g") t]
-     ["Induction              ind<C-BS>"  (insert-and-expand "ind") t]
-     ["Injection              inj<C-BS>"  (insert-and-expand "inj") t]
-     ["Intro                  i<C-BS>"  (insert-and-expand "i") t]
-     ["Intros                 is<C-BS>"  (insert-and-expand "is") t]
-     ["Intuition              intu<C-BS>"  (insert-and-expand "intu") t]
-     ["Inversion              inv<C-BS>"  (insert-and-expand "inv") t]
-     ["Omega                  om<C-BS>"  (insert-and-expand "om") t]
-     ["Pose                   po<C-BS>"  (insert-and-expand "om") t]
-     ["Reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
-     ["Replace                rep<C-BS>"  (insert-and-expand "rep") t]
-     ["Rewrite                r<C-BS>"  (insert-and-expand "r") t]
-     ["Rewrite in             ri<C-BS>"  (insert-and-expand "ri") t]
-     ["Rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
-     ["Rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") t]
-     ["Simpl                  s<C-BS>"  (insert-and-expand "s") t]
-     ["Simpl                  si<C-BS>"  (insert-and-expand "si") t]
-     ["Split                  sp<C-BS>"  (insert-and-expand "sp") t]
-     ["Subst                  su<C-BS>"  (insert-and-expand "su") t]
-     ["Symmetry               sym<C-BS>"  (insert-and-expand "sym") t]
-     ["Transitivity           trans<C-BS>"  (insert-and-expand "trans") t]
-     ["Trivial                t<C-BS>"  (insert-and-expand "t") t]
-     ["Tauto                  ta<C-BS>"  (insert-and-expand "ta") t]
-     ["Unfold                 u<C-BS>"  (insert-and-expand "u") t]
-     )
-
-    ["What are those highlighted chars??" (holes-short-doc) t]
-    ("holes" 
-     "make a hole active   click on it"
-     "disable a hole   click on it (button 2)"
-     "destroy a hole   click on it (button 3)"
-     "make a hole with mouse  C-M-select"
-     ["make a hole at point   C-M-h"  (set-make-active-hole) t]
-     ["make selection a hole  C-M-h"  (set-make-active-hole) t]
-     ["replace active hole by selection C-M-y"  (replace-update-active-hole) t]
-     "replace active hole with mouse  C-M-Shift select"
-     ["jump to active hole M-return"  (set-point-next-hole-destroy) t]
-     ["forget all holes in this buffer"  (clear-all-buffer-holes) t]
-     ["What are those holes?" (holes-short-doc) t]
-     )
-    ["expand abbrev at point" expand-abbrev t]
-    ["list abbrevs" list-abbrevs t]
-    ["Print..." coq-Print t]
-    ["Check..." coq-Check t]
-    ["Hints" coq-PrintHint t]
-    ["Show ith goal..." coq-Show t]
-    ["Search isos/pattern..." coq-SearchIsos t]
-    ["Compile" coq-Compile t] ))
-
-(provide 'coq-abbrev-V7)
-
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 7a5c584d..27544e1d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -3,120 +3,71 @@
 ;; Authors: Thomas Kleymann and Healfdene Goguen
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
 
-;; To be added for coq 7.4:
-
-;;"And" -> ???
-
 ;; $Id$
 
 (require 'proof-syntax)
 
 ;; da 15/2/03: without defvars compilation breaks
 ;; This may have broken some of logic below
-(defvar coq-version-is-V74 nil)
-(defvar coq-version-is-V7 nil)
 
+;; Pierre: we will have both versions V8.0 and V8.1 during a while the
+;; test with "coqtop -v" can be skipped if one of the variables
+;; coq-version-is-V8-0/1 is already set (useful for people dealing
+;; with several version of coq).
 
-;; Pierre: we will have both versions V6 and V7 during a while the test with "coqtop
-;; -v" can be skipped if the variable coq-version-is-V7 is already set (useful for
-;; people dealing with several version of coq) We also have coq-version-is-V74, to
-;; deal with the new module system
+; this one is temporary, for compatibility
+(defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.")
 
-(defvar coq-version-is-V6 nil 
+(defvar coq-version-is-V8-0 nil 
 "This variable can be set to t to force ProofGeneral to coq version
-coq-6.x. To do that, put (setq coq-version-is-V6 t) in your .emacs and
-restart emacs. This variable overrides coq-version-is-V7, V8 and
-V74. If none of these 3 variables is set to t, then ProofGeneral
-guesses the version of coq by doing 'coqtop -v'.")
-
-(defvar coq-version-is-V7 nil 
-"This variable can be set to t to force ProofGeneral to coq version
-between coq-7.0 and coq-7.3.1. To do that, put (setq coq-version-is-V7
-t) in your .emacs and restart emacs. This variable overrides
-coq-version-is-V74 and V8 and is overrriden by coq-version-is-V6.  If
-none of these 3 variables is set to t, then ProofGeneral guesses the
-version of coq by doing 'coqtop -v'.")
-
-(defvar coq-version-is-V74 nil 
-"This variable can be set to t to force ProofGeneral to coq version
-coq-7.4. To do that, put (setq coq-version-is-V74 t) in your .emacs
-and restart emacs. This variable is overrriden by coq-version-is-V6
-and coq-version-is-V7. If none of these 3 variables is set to t, then
-ProofGeneral guesses the version of coq by doing 'coqtop -v'. If this
-variable is put to t (before PG is loaded) then V7 is automatically
-put to t."  )
-
-(defvar coq-version-is-V8 nil 
-"This variable can be set to t to force ProofGeneral to coq version
-above coq-8.0beta. To do that, put (setq coq-version-is-V8 t) in your
-.emacs and restart emacs. This variable is overrriden by
-coq-version-is-V6, coq-version-is-V7 and coq-version-is-V74. If none
-of these 4 variables is set to t, then ProofGeneral guesses the
-version of coq by doing 'coqtop -v'. If this variable is put to t
-\(before PG is loaded) then V74 is automatically put to t." )
-
-
-
-;; only coq-version-is-V74 and coq-version-is-V7 are used later (V6
-;; corresponds to v7=nil and v74=nil)
-
+coq-8.0. To do that, put (setq coq-version-is-V8-0 t) in your .emacs and
+restart emacs. This variable cannot be true simultaneously with
+coq-version-is-V8-1. If none of these 2 variables is set to t, then
+ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
+
+(defvar coq-version-is-V8-1 nil 
+  "This variable can be set to t to force ProofGeneral to coq version
+coq-8.1 (use it for coq-8.0cvs after january 2005). To do that, put
+(setq coq-version-is-V8-1 t) in your .emacs and restart emacs. This
+variable cannot be true simultaneously with coq-version-is-V8-0. If
+none of these 2 variables is set to t, then ProofGeneral guesses the
+version of coq by doing 'coqtop -v'." )
+
+;;FIXME: how to make compilable?
 (unless (noninteractive);; DA: evaluating here gives error during compile
-  (let* ((seedoc " (to force another version, do for example C-h v coq-version-is-V7)")
-			(v8 (concat "proofgeneral is in coq 8 mode" seedoc))
-			(v74 (concat "proofgeneral is in coq 7.4 mode" seedoc))
-			(v7 (concat "proofgeneral is in coq > 6 and =< 7.3 mode" seedoc))
-			(v6 (concat "proofgeneral is in coq V6 mode" seedoc)))
+  (let* 
+		(
+		 (seedoc (concat " (to force another version, see for example"
+							  " C-h v `coq-version-is-V8-0)'."))
+		 (v80 (concat "proofgeneral is in coq 8.0 mode" seedoc))
+		 (v81 (concat "proofgeneral is in coq 8.1 mode" seedoc))
+		 (err (concat "Both config variables coq-version-is-V8-1 and"
+						  " coq-version-is-V8-0 are set to true. This is"
+						  "contradictory.")))
+	 
 	 (cond
-	  (coq-version-is-V8 
-		(message v8) 
-		(setq coq-version-is-V74 t))
-	  (coq-version-is-V74 
-		(message v74) 
-		(setq coq-version-is-V8 nil)
-		(setq coq-version-is-V7 t))
-	  (coq-version-is-V7  
-		(message v7)  
-		(setq coq-version-is-V74 nil)
-		(setq coq-version-is-V8 nil))
-	  (coq-version-is-V6  
-		(message v6)  
-		(setq coq-version-is-V8 nil) 
-		(setq coq-version-is-V74 nil) 
-		(setq coq-version-is-V7 nil))
-	  (t 
-		(let ((str (shell-command-to-string 
-						(concat coq-prog-name " -v"))))
+	  ((and coq-version-is-V8-1 coq-version-is-V8-0) 
+		(error err))
+	  (coq-version-is-V8-1 (message v81))
+	  (coq-version-is-V8-0 (message v80))
+	  (coq-version-is-V8 (setq coq-version-is-V8-0 t coq-version-is-V8-1 nil)
+								(message v80))
+	  (t;; otherwise do coqtop -v and see which version we have
+		(let ((str (shell-command-to-string (concat coq-prog-name " -v"))))
 		  ;; this match sets match-string below
 		  (string-match "version \\([.0-9]*\\)" str)
+		  (message str)
 		  (let ((num (match-string 1 str)))
-		  ;; da: added this to avoid type error in case coq command fails
-		  (if (null num) (setq num ""))
-		  (cond
-			((string-match "\\<6." num) 
-			 (message v6)
-			 (setq coq-version-is-V7 nil) 
-			 (setq coq-version-is-V74 nil))
-			((or (string-match "\\<7.0" num) 
-				  (string-match "\\<7.1" num) 
-				  (string-match "\\<7.2" num) 
-				  (string-match "\\<7.3" num)) 
-			 (message v7) 
-			 (setq coq-version-is-V7 t)
-			 (setq coq-version-is-V74 nil))
-			((string-match "\\<7.4" num) 
-			 (message v74)
-			 (setq coq-version-is-V74 t)
-			 (setq coq-version-is-V7 t) )
-			((string-match "\\<8." num) 
-			 (message v8)
-			 (setq coq-version-is-V8 t)
-			 (setq coq-version-is-V7 t) 
-			 (setq coq-version-is-V74 t))			
-			(t
-			 (message (concat "Falling back to default: " v8))
-			 (setq coq-version-is-V8 t)
-			 (setq coq-version-is-V7 t) 
-			 (setq coq-version-is-V74 t)))))))))
+			 ;; da: added this to avoid type error in case coq command fails
+			 (if (null num) (setq num ""))
+			 (cond
+			  ((or (string-match "\\<8.1" num)) 
+				(message v81)
+				(setq coq-version-is-V8-1 t))			
+			  (t ;; temporary, should be 8.1 when it is officially out
+				(message (concat "Falling back to default: " v80))
+				(setq coq-version-is-V8-0 t)
+				))))))))
 
 ;; ----- keywords for font-lock.
 
@@ -154,33 +105,22 @@ version of coq by doing 'coqtop -v'. If this variable is put to t
     "Structure"
 	 "Ltac"))
 
-;; Modules are like section in v > 7.4.
+;; Modules are like sections
 (defvar coq-keywords-goal
-  (if (or coq-version-is-V74 coq-version-is-V8)
-		'("Add\\s-+Morphism"
-		  "Chapter"
-	"Declare\\s-+Module" ;;only if not followed by:=(see coq-proof-mode-p in coq.el)
-		  "Module"
-		  "Module\\s-+Type"
-		  "Section"
-		  "Correctness"
-	"Definition" ;; only if not followed by := (see coq-proof-mode-p in coq.el)
-		  "Fact"
-		  "Goal"
-		  "Lemma"
-		  "Local"
-		  "Remark"
-	"Theorem")
-	 '("Chapter"
-		"Correctness"
-      "Definition" ;; only if not followed by := (see coq-proof-mode-p in coq.el)
-		"Fact"
-		"Goal"
-		"Lemma"
-		"Local"
-		"Remark"
-		"Section"
-		"Theorem")))
+  '("Add\\s-+Morphism"
+	 "Chapter"
+	 "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el)
+	 "Module"
+	 "Module\\s-+Type"
+	 "Section"
+	 "Correctness"
+	 "Definition";; only if not followed by := (see coq-proof-mode-p in coq.el)
+	 "Fact"
+	 "Goal"
+	 "Lemma"
+	 "Local"
+	 "Remark"
+	 "Theorem"))
 
 ;; FIXME da: this one function breaks the nice configuration of Proof General:
 ;; would like to have proof-goal-regexp instead.
@@ -239,8 +179,6 @@ of STRG matching REGEXP. Empty match are counted once."
   )
 
 
-
-
 (defvar coq-keywords-save-strict
   '("Defined"
     "Save"
@@ -373,7 +311,6 @@ Print and Check commands, put the following line in your .emacs:
 	 "Hint\\s-+Unfold"
 	 "Hint\\s-+Extern"
 	 "Hint\\s-+Constructors"
-    "Hints" ;no more a keyword in v8
     "Identity\\s-+Coercion"
     "Implicit\\s-+Arguments\\s-+Off"
     "Implicit\\s-+Arguments\\s-+On"
@@ -429,6 +366,42 @@ Print and Check commands, put the following line in your .emacs:
 			 coq-keywords-state-preserving-commands)
   "All commands keyword.")
 
+(defvar coq-tacticals
+  '("abstract"
+	 "do"
+	 "idtac" ;; also in state-preserving-tactic
+	 "fail"
+	 "orelse"
+	 "repeat"
+	 "try"
+	 "Time")
+  "Keywords for tacticals in a Coq script.")
+
+; From JF Monin:
+(defvar coq-reserved
+  '("False"
+	 "True"
+	 "after"
+	 "as"
+	 "cofix"
+	 "fix"
+	 "forall"
+	 "fun"
+	 "match"
+	 "return"
+	 "struct"
+    "else"
+    "end"
+    "if"
+    "in"
+    "into"
+    "let"
+    "then"
+    "using"
+    "with"
+	 )
+  "Reserved keywords of Coq.")
+
 
 (defcustom coq-user-state-changing-tactics nil
   "List of user defined Coq tactics that need to be backtracked;
@@ -442,205 +415,112 @@ Intro and Elim tactics, put the following line in your .emacs:
   :group 'coq)
 
 (defvar coq-state-changing-tactics
- 
- (cond
-  (coq-version-is-V8 
-	(append  '("absurd"
-	    "apply"
-	    "assert"
-	    "assumption"
-	    "auto"
-	    "autorewrite"
-	    "case"
-	    "cbv"
-	    "change"
-	    "clear"
-	    "clearbody"
-	    "cofix"
-	    "compare"
-	    "compute"
-		 "congruence"
-	    "constructor"
-	    "contradiction"
-	    "cut"
-	    "cutrewrite"
-	    ;;"dhyp"
-	    ;;"dind"
-	    "decide equality"
-	    "decompose"
-	    "dependent inversion"
-	    "dependent inversion_clear"
-	    "dependent rewrite ->"
-	    "dependent rewrite <-"
-	    "dependent\\s-+inversion"
-	    "dependent\\s-+inversion_clear"
-	    "destruct"
-	    "discrr"
-	    "discriminate"
-	    "double\\s-+induction"
-	    "eapply"
-	    "eauto"
-		 "econstructor"
-		 "eleft"
-		 "eright"
-		 "esplit"
-		 "eexists"
-	    "elim"
-	    "elimtype"
-	    "exact"
-	    "exists"
-	    "field"
-		 "firstorder"
-	    "fix"
-	    "fold"
-	    "fourier"
-	    "generalize"
-	    "hnf"
-	    "induction"
-	    "coinduction"
-	    "injection"
-		 "instantiate"
-	    "intro[s]?"
-	    "intuition"
-	    "inversion"
-	    "inversion_clear"
-		 "jp"
-	    "lapply"
-	    "lazy"
-	    "left"
-	    "lettac"
-	    "linear"
-	    "load"
-	    "move"
-	    "newdestruct"
-	    "newinduction"
-	    "omega "
-	    "pattern"
-	    "pose"
-	    "program"
-	    "program_all"
-	    "prolog"
-	    "quote"
-	    "realizer"
-	    "red"
-	    "refine"
-	    "reflexivity"
-	    "rename"
-	    "replace"
-	    "resume"
-	    "rewrite"
-	    "right"
-	    "ring"
-		 "set"
-	    "setoid_replace"
-	    "simpl"
-	    "simple\\s-+inversion"
-	    "simplify_eq"
-	    "specialize"
-	    "split"
-	    "splitabsolu"
-	    "splitrmult"
-	    "suspend"
-		 "subst"
-	    "symmetry"
-	    "tauto"
-	    "transitivity"
-	    "trivial"
-	    "unfold"
-		 "functional\\s-+induction")
-	  coq-user-state-changing-tactics))
-  (t 
-	(append  '("Absurd"
-	    "Apply"
-	    "Assert"
-	    "Assumption"
-	    "Auto"
-	    "AutoRewrite"
-	    "Case"
-	    "Cbv"
-	    "Change"
-	    "Clear"
-	    "ClearBody"
-	    "Cofix"
-	    "Compare"
-	    "Compute"
-	    "Constructor"
-	    "Contradiction"
-	    "Cut"
-	    "CutRewrite"
-	    ;;"DHyp"
-	    ;;"DInd"
-	    "Decide Equality"
-	    "Decompose"
-	    "Dependent Inversion"
-	    "Dependent Inversion_clear"
-	    "Dependent Rewrite ->"
-	    "Dependent Rewrite <-"
-	    "Dependent\\s-+Inversion"
-	    "Dependent\\s-+Inversion_clear"
-	    "Destruct"
-	    "DiscrR"
-	    "Discriminate"
-	    "Double\\s-+Induction"
-	    "EApply"
-	    "EAuto"
-	    "Elim"
-	    "ElimType"
-	    "Exact"
-	    "Exists"
-	    "Field"
-	    "Fix"
-	    "Fold"
-	    "Fourier"
-	    "Generalize"
-	    "Hnf"
-	    "Induction"
-	    "Injection"
-	    "Intro[s]?"
-	    "Intuition"
-	    "Inversion"
-	    "Inversion_clear"
-	    "LApply"
-	    "Lazy"
-	    "Left"
-	    "LetTac"
-	    "Linear"
-	    "Load"
-	    "Move"
-	    "NewDestruct"
-	    "NewInduction"
-	    "Omega "
-	    "Pattern"
-	    "Pose"
-	    "Program"
-	    "Program_all"
-	    "Prolog"
-	    "Quote"
-	    "Realizer"
-	    "Red"
-	    "Refine"
-	    "Reflexivity"
-	    "Rename"
-	    "Replace"
-	    "Resume"
-	    "Rewrite"
-	    "Right"
-	    "Ring"
-	    "Setoid_replace"
-	    "Simpl"
-	    "Simple Inversion"
-	    "Simplify_eq"
-	    "Specialize"
-	    "Split"
-	    "SplitAbsolu"
-	    "SplitRmult"
-	    "Suspend"
-	    "Symmetry"
-	    "Tauto"
-	    "Transitivity"
-	    "Trivial"
-	    "Unfold")
-	  coq-user-state-changing-tactics))))
+  (append  
+	'(
+	  "absurd"
+	  "apply"
+	  "assert"
+	  "assumption"
+	  "auto"
+	  "autorewrite"
+	  "case"
+	  "cbv"
+	  "change"
+	  "clear"
+	  "clearbody"
+	  "cofix"
+	  "compare"
+	  "compute"
+	  "congruence"
+	  "constructor"
+	  "contradiction"
+	  "cut"
+	  "cutrewrite"
+	  ;;"dhyp"
+	  ;;"dind"
+	  "decide equality"
+	  "decompose"
+	  "dependent inversion"
+	  "dependent inversion_clear"
+	  "dependent rewrite ->"
+	  "dependent rewrite <-"
+	  "dependent\\s-+inversion"
+	  "dependent\\s-+inversion_clear"
+	  "destruct"
+	  "discrr"
+	  "discriminate"
+	  "double\\s-+induction"
+	  "eapply"
+	  "eauto"
+	  "econstructor"
+	  "eleft"
+	  "eright"
+	  "esplit"
+	  "eexists"
+	  "elim"
+	  "elimtype"
+	  "exact"
+	  "exists"
+	  "field"
+	  "firstorder"
+	  "fix"
+	  "fold"
+	  "fourier"
+	  "generalize"
+	  "hnf"
+	  "induction"
+	  "coinduction"
+	  "injection"
+	  "instantiate"
+	  "intro[s]?"
+	  "intuition"
+	  "inversion"
+	  "inversion_clear"
+	  "jp"
+	  "lapply"
+	  "lazy"
+	  "left"
+	  "lettac"
+	  "linear"
+	  "load"
+	  "move"
+	  "newdestruct"
+	  "newinduction"
+	  "omega "
+	  "pattern"
+	  "pose"
+	  "program"
+	  "program_all"
+	  "prolog"
+	  "quote"
+	  "realizer"
+	  "red"
+	  "refine"
+	  "reflexivity"
+	  "rename"
+	  "replace"
+	  "resume"
+	  "rewrite"
+	  "right"
+	  "ring"
+	  "set"
+	  "setoid_replace"
+	  "simpl"
+	  "simple\\s-+inversion"
+	  "simplify_eq"
+	  "specialize"
+	  "split"
+	  "splitabsolu"
+	  "splitrmult"
+	  "suspend"
+	  "subst"
+	  "symmetry"
+	  "tauto"
+	  "transitivity"
+	  "trivial"
+	  "unfold"
+	  "functional\\s-+induction")
+	coq-user-state-changing-tactics))
 
 (defcustom coq-user-state-preserving-tactics nil
   "List of user defined Coq tactics that do not need to be backtracked;
@@ -672,66 +552,6 @@ Idtac (Nop) tactic, put the following line in your .emacs:
 	  coq-keywords-defn coq-keywords-commands)
   "All keywords in a Coq script.")
 
-(defvar coq-tacticals
-  (cond 
-	(coq-version-is-V8 
-	 '("abstract"
-		"do"
-		"idtac"									 ; also in  state-preserving-tactic
-		"fail"
-		"orelse"
-		"repeat"
-		"try"
-		"Time"))
-	(t '("Abstract"
-		  "Do"
-		  "Idtac"								 ; also in  state-preserving-tactic
-		  "Fail"
-		  "Orelse"
-		  "Repeat"
-		  "Try"
-		  "Time")))
-  "Keywords for tacticals in a Coq script.")
-
-; From JF Monin:
-(defvar coq-reserved-common
-  '("as"
-	 "True"
-	 "False"
-    "else"
-    "end"
-    "if"
-    "in"
-    "into"
-    "let"
-    "then"
-    "using"
-    "with"
-	 "after")
-  "Reserved keywords of Coq.")
-
-(defvar coq-reserved-V8
-  '(
-	 "cofix"
-	 "fix"
-	 "struct"
-	 "match"
-	 "forall"
-	 "fun"
-	 "return"
-	 ))
-
-(defvar coq-reserved-V7
-  '(
-	 "ALL" "Cases" "EX" "Fix" "of" "CoFix"
-	 ))
-
-(defvar coq-reserved 
-  (cond
-	(coq-version-is-V8 
-	 (append coq-reserved-common coq-reserved-V8))
-	(t 
-	 (append coq-reserved-common coq-reserved-V7))))
 
 
 (defvar coq-symbols
diff --git a/coq/coq.el b/coq/coq.el
index 9bdee65b..1d10a246 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -40,25 +40,24 @@ To disable coqc being called (and use only make), set this to nil."
 (require 'coq-indent)
 
 ;; 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.\n Implicit Arguments Off. ")
+(defconst coq-shell-restart-cmd "Reset Initial.\n ")
 
 
 ;; NB: da: PG 3.5: added \n here to account for blank line
 ;; in Coq output.  (FIXME: Is this OK in Coq pre 8.x?)
 ;; Better result for shrinking windows, grabbing shell output
-(defvar coq-shell-prompt-pattern (concat "^\n?" proof-id " < ")
+;; Pierre added the state number here, this is new in Coq.
+
+; patch provisoire envoye a coqdev:
+;(defvar coq-shell-prompt-pattern (concat "^\n?" proof-id " < "  "\\(?:\\*[0-9]+\\)?")
+(defvar coq-shell-prompt-pattern 
+  (concat "^\n?" proof-id " < "  "\\(?:\\*[0-9]+\\)?")
   "*The prompt pattern for the inferior shell running coq.")
 
 ;; FIXME da: this was disabled (set to nil) -- why?
 ;; da: 3.5: add experimetntal
 (defvar coq-shell-cd 
-  (if coq-version-is-V8 
-      "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
-    "Cd \"%s\"")
+  "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
   "*Command of the inferior process to change the directory.")
 
 (defvar coq-shell-abort-goal-regexp "Current goal aborted"
@@ -101,13 +100,7 @@ To disable coqc being called (and use only make), set this to nil."
 
 ;; ----- coq specific menu is defined in coq-abbrev.el
 
-(cond
- (coq-version-is-V8 (require 'coq-abbrev))
- (t (require 'coq-abbrev-V7))
- )
-
-
-
+(require 'coq-abbrev)
 
 (defun coq-insert-section (s)
   (interactive  "sSection name: ")
@@ -173,15 +166,15 @@ To disable coqc being called (and use only make), set this to nil."
   (proof-ids-to-regexp coq-keywords-state-changing-commands))
 (defconst coq-state-preserving-commands-regexp 
   (proof-ids-to-regexp coq-keywords-state-preserving-commands))
+(defconst coq-commands-regexp 
+  (proof-ids-to-regexp coq-keywords-commands))
 (defvar coq-retractable-instruct-regexp 
   (proof-ids-to-regexp coq-retractable-instruct))
 (defvar coq-non-retractable-instruct-regexp
   (proof-ids-to-regexp coq-non-retractable-instruct))
 
 (defvar coq-keywords-section
-  (cond 
-   (coq-version-is-V74 '("Section" "Module\\-+Type" "Declare\\s-+Module" "Module"))
-   (t '("Section"))))
+  '("Section" "Module\\-+Type" "Declare\\s-+Module" "Module"))
 
 (defvar coq-section-regexp 
   (concat "\\(" (proof-ids-to-regexp coq-keywords-section) "\\)")
@@ -219,22 +212,15 @@ To disable coqc being called (and use only make), set this to nil."
 (defun coq-set-undo-limit (undos)
   (proof-shell-invisible-command (format "Set Undo %s. " undos)))
 
-;;
-;; FIXME Papageno 05/1999: must take sections in account.
-;;
 ;; da: have now combined count-undos and find-and-forget, they're the
 ;; same now we deal with nested proofs and send general sequence
-;; "Abort. ... Abort. Back n. Undo n."
+;; "Abort. ... Abort. BackTo n. Undo n."
 ;;
 
 (defconst coq-keywords-decl-defn-regexp
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
   "Declaration and definition regexp.")
 
-; Pierre: This is a try, for use in find-and-forget. It seems to work but 
-; is it correct with respect to the asynchronous communication between Coq 
-; and emacs?  
-; DA: should be okay, communication is not as asynchronous as you think
 (defun coq-proof-mode-p ()
   "Allows to know if we are currentlly in proof mode. 
 Look at the last line of the *coq* buffer to see if the prompt is the
@@ -243,9 +229,6 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
   (not (string-match "^Coq < " proof-shell-last-prompt)))
 
 
-;; Pierre: May 29 2002 added a "Back n. " command in order to
-;; synchronize more accurately.
- 
 ;; DA: rewrote to combine behaviour with count-undos, to work with
 ;; nested proofs.
 
@@ -266,8 +249,23 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
 (defun coq-state-preserving-command-p (str)
   (proof-string-match (concat "\\`\\(" coq-state-preserving-commands-regexp "\\)") str))
 
+(defun coq-command-p (str)
+  (proof-string-match (concat "\\`\\(" coq-commands-regexp "\\)") str))
+
 (defun coq-state-preserving-tactic-p (str)
-  (proof-string-match (concat "\\`\\(" coq-state-preserving-tactics-regexp "\\)") str))
+  (proof-string-match 
+   (concat "\\`\\(" 
+           coq-state-preserving-tactics-regexp "\\)") str))
+
+(defun coq-state-changing-tactic-p (str) ; unknown things are considered (state
+                                        ;changing) tactics here
+  (and (not (coq-command-p str)) 
+       (not (coq-state-preserving-tactic-p str)))
+  )
+;  (proof-string-match 
+;   (concat "\\(\\`\\|\\`abstract\\s-+\\)\\(" 
+;           coq-state-changing-tactics-regexp "\\)") str))
+
 
 (defun coq-state-changing-command-p (str)
   (proof-string-match (concat "\\`\\(" coq-state-changing-commands-regexp "\\)") str))
@@ -280,10 +278,122 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
    (concat "\\`" coq-section-regexp 
            "\\s-+\\(" proof-id "\\)\\(\\s-*\\(" proof-id "\\)\\)?") str)) 
 
-;;(span-at (point) 'type)
-;;(span-property (span-at (point) 'type) 'cmd)
 
-(defun coq-find-and-forget (span)
+;;New: using the statenumber inside the coq prompte to backtrack more easily
+;;FIXME: make this more robust and faster
+(defun coq-last-statenum (s)
+  "reads the last prompt state number in the coq process buffer. It is supposed that
+  we are already in the coq buffer."
+  (let* ((lastprompt (or s (error "no prompt !!?")))
+         (s (string-match "< \\*\\([0-9]+\\)ù" lastprompt)))
+    (string-to-int (match-string 1 lastprompt))
+    )
+  )
+
+(defun coq-last-statenum-safe ()
+  "See `coq-last-statenum'."
+  (coq-last-statenum proof-shell-last-prompt)
+  )
+
+;; The state number we want to put in a span is the prompt number given *just before*
+;; the command was sent. This variable remembers this number and will be updated when
+;; used see coq-set-state-number. Initially 1 because Coq initial state has number 1.
+(defvar coq-last-but-one-statenum 1)
+
+(defun coq-get-span-statenum (span)
+  "Returns the state number of the span."
+  (span-property span 'statenum)
+  )
+
+(defun coq-set-span-statenum (span val)
+  "Sets the state number of the span to val."
+  (set-span-property span 'statenum val)
+  )
+
+(defun proof-last-locked-span () 
+  (save-excursion ;; didn't found a way to avoid buffer switching
+    (set-buffer proof-script-buffer)
+    (span-at (- (proof-locked-end) 1) 'type)
+    )
+  )
+
+;; Each time the state changes (hook below), (try to) put the state number in the
+;; last locked span (will fail if there is already a number which should happen when
+;; going back in the script).  The state number we put is not the last one because
+;; the last one has been sent by Coq *after* the change. We use
+;; `coq-last-but-one-statenum' instead and then update it.
+
+(defun coq-set-state-number ()
+  "Sets the last locked span's state number to the number found in the *last but one*
+  prompt (variable `coq-last-but-one-statenum'), unless it has already a state
+  number. Also updates `coq-last-but-one-statenum' to the last state number because
+  next time this function will be called, a new prompt will be in
+  `proof-shell-last-prompt'."
+  (if (and proof-shell-last-prompt proof-script-buffer)
+      (let ((sp (proof-last-locked-span)))
+        (unless (or (not sp) (coq-get-span-statenum sp))
+          (coq-set-span-statenum sp coq-last-but-one-statenum))
+        (setq coq-last-but-one-statenum (coq-last-statenum-safe))
+        )
+    )
+  )
+
+;; This hook seems the one we want (if we are in V8.1 mode only):
+(add-hook 'proof-state-change-hook 
+          '(lambda () (if coq-version-is-V8-1 (coq-set-state-number))))
+
+
+;; Simplified version of backtracking which uses state numbers
+(defun coq-find-and-forget-v81 (span)
+  (let (str ans (naborts 0) (nundos 0) 
+            (span-staten (coq-get-span-statenum span)))
+    ;; go from the top of the backtracked region to the bottom
+    ;; and computes naborts and nundos
+    (while (and span (not ans))
+      (setq str (span-property span 'cmd))
+      (cond
+       ((coq-is-comment-or-proverprocp span)) ; do nothing for comments
+       ;; unsaved goal --> increment naborts 
+       ;; (modules are "goals" but not here (they don't need abort, just backto, even
+       ;;  if unclosed))
+       ((and (not (coq-is-goalsave-p span)) 
+             (coq-goal-command-p str)
+             (not (coq-section-or-module-start-p str))) 
+        (incf naborts))
+       ;; if nabort<>0 then current goal is actually aborted
+       ((and (coq-proof-mode-p) (coq-state-changing-tactic-p str) (= naborts 0))
+        (incf nundos))
+       ;; default case: command, do nothing (BackTo will deal with this)
+       (t ())
+       )
+      ;;go to next span
+      (setq span (next-span span 'type))
+      )
+    (let (last-staten)
+      (setq last-staten (coq-last-statenum-safe))
+      (setq ans
+            (concat
+             (if (> naborts 0)
+                 ;; ugly, but blame Coq
+                 (let ((aborts "Abort. "))
+                   (while (> (decf naborts) 0) (setq aborts (concat "Abort. " aborts)))
+                   aborts))
+             (if (> nundos 0) 
+                 (concat "Undo " (int-to-string nundos) ". "))
+             (if (and span-staten last-staten (not (= span-staten last-staten))) 
+                 (concat "BackTo " (int-to-string span-staten) ". "))
+             ))
+      (if (string-equal ans "") proof-no-command ; not here because if
+        ;; we backtrack a state preserving command, we must do
+        ;; *nothing*, not even a CR (in v74, no prompt is returned
+        ;; with "\n")
+        ans)
+      )
+    )
+  )
+
+
+(defun coq-find-and-forget-v80 (span)
   (let (str ans (naborts 0) (nbacks 0) (nundos 0))
     (while (and span (not ans))
       (setq str (span-property span 'cmd))
@@ -319,7 +429,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
        
        ;; Unsaved goal commands: each time we hit one of these
        ;; we need to issue Abort to drop the proof state.
-       ((coq-goal-command-p str) (incf naborts))
+       ((coq-goal-command-p str) (incf naborts)) ; FIX: nundos<-0 ?
 
        ;; If we are already outside a proof, issue a Reset.  [ improvement would be
        ;; to see if the undoing will take us outside a proof, and use the first Reset
@@ -373,7 +483,15 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
 						 ; *nothing*, not even a CR (in v74, no prompt is returned
 						 ; with "\n")
       ans))))
-  
+
+;; I don't like this but it make compilation possible
+(defun coq-find-and-forget (span)
+ (cond 
+  (coq-version-is-V8-1 (coq-find-and-forget-v81 span))
+  (coq-version-is-V8-0 (coq-find-and-forget-v80 span))
+  (t (coq-find-and-forget-v80 span)) ;; this is temporary
+  )
+ )  
 
 (defvar coq-current-goal 1
   "Last goal that emacs looked at.")
@@ -404,12 +522,8 @@ This is specific to coq-mode."
   (interactive)
   (let (cmd)
     (proof-shell-ready-prover) 
-    (setq cmd (read-string 
-	       (if coq-version-is-V7 "SearchPattern: " "SearchIsos: ") 
-	       nil 'proof-minibuffer-history))
-    (proof-shell-invisible-command
-     (format (if coq-version-is-V7 "SearchPattern %s. "
-	       "SearchIsos %s. ") cmd))))
+    (setq cmd (read-string "SearchPattern: " nil 'proof-minibuffer-history))
+    (proof-shell-invisible-command (format "SearchPattern %s. " cmd))))
 
 
 (defun coq-guess-or-ask-for-string (s)
@@ -611,7 +725,8 @@ Based on idea mentioned in Coq reference manual."
                                 (if coq-translate-to-v8 " -translate")))
   (setq proof-mode-for-shell    'coq-shell-mode)
   (setq proof-mode-for-goals    'coq-goals-mode)
-  (setq proof-mode-for-response 'coq-response-mode))
+  (setq proof-mode-for-response 'coq-response-mode)
+  )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Configuring proof and pbp mode and setting up various utilities  ;;
@@ -620,11 +735,8 @@ Based on idea mentioned in Coq reference manual."
 (defun coq-mode-config ()
 
   (setq proof-terminal-char ?\.)
-  (setq proof-script-command-end-regexp
-        (if coq-version-is-V7 
-;            "\\(?:\\w\\|\\s-\\|\\s)\\|\\\\*\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
-            "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)"
-          "[.]"))
+  (setq proof-script-command-end-regexp 
+        "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)")
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
   (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name
@@ -649,9 +761,9 @@ Based on idea mentioned in Coq reference manual."
   (setq proof-kill-goal-command nil)
 
   (setq proof-goal-command-p 'coq-goal-command-p
-	proof-find-and-forget-fn 'coq-find-and-forget
+        proof-find-and-forget-fn 'coq-find-and-forget
         pg-topterm-goalhyp-fn 'coq-goal-hyp
-	proof-state-preserving-p 'coq-state-preserving-p)
+        proof-state-preserving-p 'coq-state-preserving-p)
 
   (setq proof-save-command-regexp coq-save-command-regexp
         proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>.
@@ -677,13 +789,8 @@ Based on idea mentioned in Coq reference manual."
   ;; span menu 
   (setq proof-script-span-context-menu-extensions 'coq-create-span-menu)
 
-  ;;Coq V7 changes this 
-  (setq proof-shell-start-silent-cmd 
-	(if coq-version-is-V7 "Set Silent. "   "Begin Silent. ")
-	proof-shell-stop-silent-cmd  
-	(if coq-version-is-V7 "Unset Silent. " "End Silent. "))
-;  (setq proof-shell-start-silent-cmd "Begin Silent. "
-;	proof-shell-stop-silent-cmd  "End Silent. ")
+  (setq proof-shell-start-silent-cmd "Set Silent. "
+        proof-shell-stop-silent-cmd "Unset Silent. ")
 
   (coq-init-syntax-table)
   (setq comment-quote-nested nil) ;; we can cope with nested comments
@@ -787,7 +894,7 @@ Based on idea mentioned in Coq reference manual."
 ;; Updated and simplified for Coq 8, PG 3.5 (22.04.04) by DA.
 
 ;; First note that coq-shell-cd is sent whenever we activate scripting, 
-;; for V8 it extends the loadpath with the current directory.
+;; it extends the loadpath with the current directory.
 
 ;; When scripting is turned off, we compile the file to update the .vo.
 (defun coq-maybe-compile-buffer ()