diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2008-01-30 09:36:28 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2008-01-30 09:36:28 +0000 |
| commit | 55e2be93dcbb1f9d0b0bf44157eae684672c77be (patch) | |
| tree | a6362ad9c2495ef65a3683fcb8d9453e9855ba4e /coq | |
| parent | adf9bc400b341c4e1d3bea84fede9839468e6f91 (diff) | |
coq : changing highlight of solve, adding Export
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index ad51d990..bd6dce18 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -350,6 +350,7 @@ ("omega" "o" "omega" t "omega") ("reflexivity" "refl" "reflexivity #" t "reflexivity") ("ring" "ring" "ring #" t "ring") + ("solve" nil "solve [ # | # ]" nil "solve") ("tauto" "ta" "tauto" t "tauto") )) "Coq tactic(al)s that solve a subgoal." @@ -361,7 +362,6 @@ coq-user-tacticals-db '( ("info" nil "info #" nil "info") - ("solve" nil "solve [ # | # ]" nil "solve") ("first" nil "first [ # | # ]" nil "first") ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") ("do" nil "do @{num} @{tac}" nil "do") @@ -513,6 +513,7 @@ ("Comments" nil "Comments #." nil "Comments") ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) ("Eval" nil "Eval #." nil "Eval") + ("Export" nil "Export #." t "Export") ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") |