aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2002-07-27 16:50:29 +0000
committerPierre Courtieu2002-07-27 16:50:29 +0000
commit16d4b3d93aef3c0d4af887edf2ccab8c86400e44 (patch)
tree5e67ade898b6060bb1b484ffc64fc2e3d7f753e5
parent325784e32122802b42aff7254423db0ca9509fb4 (diff)
Finished the changing of names of config. variables (coq-user...).
-rw-r--r--coq/coq-syntax.el12
-rw-r--r--coq/coq.el4
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