From 55e2be93dcbb1f9d0b0bf44157eae684672c77be Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Wed, 30 Jan 2008 09:36:28 +0000
Subject: coq : changing highlight of solve, adding Export

---
 coq/coq-syntax.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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")
-- 
cgit v1.2.3