diff options
| author | Pierre Courtieu | 2002-07-27 16:50:29 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2002-07-27 16:50:29 +0000 |
| commit | 16d4b3d93aef3c0d4af887edf2ccab8c86400e44 (patch) | |
| tree | 5e67ade898b6060bb1b484ffc64fc2e3d7f753e5 | |
| parent | 325784e32122802b42aff7254423db0ca9509fb4 (diff) | |
Finished the changing of names of config. variables (coq-user...).
| -rw-r--r-- | coq/coq-syntax.el | 12 | ||||
| -rw-r--r-- | 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 @@ -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 |
