From 16d4b3d93aef3c0d4af887edf2ccab8c86400e44 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Sat, 27 Jul 2002 16:50:29 +0000
Subject: Finished the changing of names of config. variables (coq-user...).

---
 coq/coq-syntax.el | 12 ++++++------
 coq/coq.el        |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 7234d53b..6811e1b3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -237,7 +237,7 @@ Print and Check commands, put the following line in your .emacs:
   "All commands keyword")
 
 
-(defcustom coq-user-undoable-tactics nil
+(defcustom coq-user-state-changing-tactics nil
  
 "Configuration variable (default to nil). List of strings containing
 the user defined Coq tactics that need to be backtracked (like almost
@@ -246,12 +246,12 @@ all tactics, but \"Idtac\" (\"Proof\" is a command actually)).
 For example if MyIntro and MyElim are user defined variants of the
 Intro and Elim tactics, put the following line in your .emacs:
 
-(setq coq-user-undoable-tactics
+(setq coq-user-state-changing-tactics
 		'(\"MyIntro\" \"MyElim\"))
 "
 )
 
-(defvar coq-undoable-tactics
+(defvar coq-state-changing-tactics
  (append  '(
 "Absurd"
 "Apply"
@@ -344,7 +344,7 @@ Intro and Elim tactics, put the following line in your .emacs:
 "Trivial"
 "Unfold"
 )
-coq-user-undoable-tactics
+coq-user-state-changing-tactics
 )
 
 )
@@ -372,11 +372,11 @@ Idtac (Nop) tactic, put the following line in your .emacs:
 )
 
 (defvar coq-tactics 
-  (append coq-undoable-tactics coq-state-preserving-tactics))
+  (append coq-state-changing-tactics coq-state-preserving-tactics))
 
 
 (defvar coq-retractable-instruct
-  (append coq-undoable-tactics coq-keywords-state-changing-commands)
+  (append coq-state-changing-tactics coq-keywords-state-changing-commands)
   )
 
 (defvar coq-non-retractable-instruct
diff --git a/coq/coq.el b/coq/coq.el
index 11c9fded..e41a1154 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -117,8 +117,8 @@
 
 
 
-(defconst coq-undoable-tactics-regexp 
-  (proof-ids-to-regexp coq-undoable-tactics))
+(defconst coq-state-changing-tactics-regexp 
+  (proof-ids-to-regexp coq-state-changing-tactics))
 (defconst coq-state-preserving-tactics-regexp 
   (proof-ids-to-regexp coq-state-preserving-tactics))
 (defconst coq-tactics-regexp
-- 
cgit v1.2.3