diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-04-15 13:57:48 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-15 13:57:48 +0000 |
| commit | 353217b0ec53f768db348a75b0faedc162bebcda (patch) | |
| tree | b4b7829d0d552ea39ed5472bead587c16a3a691c /coq | |
| parent | 7ea8d341909787f8b95550f5186493666d032066 (diff) | |
added some tactical names for coq.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index d7684506..a06ebcc9 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -671,12 +671,24 @@ Idtac (Nop) tactic, put the following line in your .emacs: "All keywords in a Coq script.") (defvar coq-tacticals - '("Abstract" - "Do" - "Idtac" ; also in state-preserving-tactic - "Orelse" - "Repeat" - "Try") + (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: |