Added some more syntax keywords. Made admit tactic with its own red

culpabilizing face.

2 files changed, 55 insertions, 1 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 4b8d53cd..8c2b28a7 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -235,10 +235,23 @@ See `coq-syntax-db' for DB structure."
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
+;;A new face for tactics which fail when they don't kill the current goal
+(defface coq-cheat-face
+  (proof-face-specs
+   (:background "red") ; pour les fonds clairs
+   (:background "red") ; pour les fond foncés
+   ()) ; pour le noir et blanc
+  "Face for names of closing tactics in proof scripts."
+  :group 'proof-faces)
+
 (defconst coq-solve-tactics-face 'coq-solve-tactics-face
   "Expression that evaluates to a face.
 Required so that 'proof-solve-tactics-face is a proper facename")
 
+(defconst coq-cheat-face 'coq-cheat-face
+  "Expression that evaluates to a face.
+Required so that 'proof-solve-tactics-face is a proper facename")
+
 
 
 (provide 'coq-db)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 8bd2a715..6fe193ed 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -100,6 +100,23 @@ See also `coq-prog-env' to adjust the environment."
   :type '(repeat sexp)
   :group 'coq)
 
+(defcustom coq-user-cheat-tactics-db nil
+  "User defined closing tactics BY CHEATING (ex: admit).
+ See `coq-syntax-db' for syntax. It is not necessary to add your
+ own commands here (it is not needed by the
+ synchronizing/backtracking system). You may however do so for
+ the following reasons:
+
+   1 your commands will be colorized by font-lock
+
+   2 your commands will be added to the menu and to completion when
+   calling \\[coq-insert-command]
+
+   3 you may define an abbreviation for your command."
+
+  :type '(repeat sexp)
+  :group 'coq)
+
 
 
 (defcustom coq-user-reserved-db nil
@@ -137,6 +154,8 @@ See also `coq-prog-env' to adjust the environment."
      ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t)
      ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite")
      ("case" "c" "case " t "case")
+     ("case_eq" "ceq" "case_eq " t "case_eq")
+     ("case_type" "cty" "case_type " t "case_type")
      ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv")
      ("change in" "chi" "change # in #" t)
      ("change with in" "chwi" "change # with # in #" t)
@@ -191,6 +210,7 @@ See also `coq-prog-env' to adjust the environment."
      ("fold" "fold" "fold #" t "fold")
      ;;     ("fourier" "four" "fourier" t "fourier")
      ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction")
+     ("functional inversion" "finv" "functional inversion @{H}" t "functional\\s-+inversion")
      ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent")
      ("generalize" "g" "generalize #" t "generalize")
      ("hnf" "hnf" "hnf" t "hnf")
@@ -298,6 +318,17 @@ See also `coq-prog-env' to adjust the environment."
   "Coq tactic(al)s that solve a subgoal."
   )
 
+(defvar coq-solve-cheat-tactics-db
+  (append
+   coq-user-cheat-tactics-db
+   '(
+     ("admit" nil "admit" t "admit")
+     ))
+  "Coq tactic(al)s that solve a subgoal."
+  )
+
+
+
 
 (defvar coq-tacticals-db
   (append
@@ -333,6 +364,7 @@ See also `coq-prog-env' to adjust the environment."
     ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite")
     ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t )
     ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold")
+    ("Existing Instance" nil "Existing Instance " t "Existing\\s-+Instance")
     ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis")
     ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses")
     ("Parameter" "par" "Parameter #: #" t "Parameter")
@@ -406,6 +438,8 @@ See also `coq-prog-env' to adjust the environment."
 (defvar coq-goal-starters-db
   '(
     ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism")
+    ("Add Parametric Morphism" nil "Add Parametric Morphism : " t "Add\\s-+Parametric\\s-+Morphism")
+    ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation")
     ("Chapter" "chp" "Chapter # : #." t "Chapter")
     ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary")
     ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t)
@@ -434,7 +468,7 @@ See also `coq-prog-env' to adjust the environment."
    '(
      ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu
      ("About" nil "About #." nil "About")
-     ("Add" nil "Add #." nil "Add" nil t)
+;     ("Add" nil "Add #." nil "Add" nil t)
      ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring")
      ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring")
      ("Add Field" nil "Add Field #." t "Add\\s-+Field")
@@ -489,6 +523,7 @@ See also `coq-prog-env' to adjust the environment."
      ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t)
      ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local")
      ("Notation (simple)" "nots" "Notation # := #." t "Notation")
+     ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque")
      ("Opaque" nil "Opaque #." nil "Opaque")
      ("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic")
      ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
@@ -536,6 +571,7 @@ See also `coq-prog-env' to adjust the environment."
      ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width")
      ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard")
      ("Transparent" nil "Transparent #." nil "Transparent")
+
      ("Unfocus" nil "Unfocus." nil "Unfocus")
      ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline")
      ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize")
@@ -754,6 +790,10 @@ Used by `coq-goal-command-p'"
   (coq-build-regexp-list-from-db coq-solve-tactics-db)
   "Keywords for closing tactic(al)s.")
 
+(defvar coq-solve-cheat-tactics
+  (coq-build-regexp-list-from-db coq-solve-cheat-tactics-db)
+  "Keywords for closing by cheating tactic(al)s.")
+
 (defvar coq-tacticals
   (coq-build-regexp-list-from-db coq-tacticals-db)
   "Keywords for tacticals in a Coq script.")
@@ -909,6 +949,7 @@ Group number 1 matches the name of the library which is required.")
     coq-font-lock-terms
     (list
     (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face)
+    (cons (proof-ids-to-regexp coq-solve-cheat-tactics) 'coq-cheat-face)
     (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
     (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face)
     (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face)