updated CHANGES

added an example file in coq/

2 files changed, 145 insertions, 0 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index efb65114..18d2df36 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -4,7 +4,11 @@
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
 
+<<<<<<< coq-syntax.el
 ;; $Id$
+=======
+;; $Id$
+>>>>>>> 9.0
 
 (require 'proof-syntax)
 (require 'coq-db)
@@ -927,6 +931,7 @@ Used by `coq-goal-command-p'"
   "*Font-lock table for Coq terms.")
 
 
+
 ;; According to Coq, "Definition" is both a declaration and a goal.
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
@@ -953,6 +958,9 @@ Used by `coq-goal-command-p'"
   (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
  	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
 
+;;  (defconst coq-decl-with-hole-regexp
+;;    (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil))
+
 (defconst coq-defn-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-defn)
           "\\)\\s-+\\(" coq-id "\\)"))
@@ -993,6 +1001,7 @@ Used by `coq-goal-command-p'"
     (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
     ;; Remove spurious variable and function faces on commas.
     '(proof-zap-commas))))
+
 (defvar coq-font-lock-keywords coq-font-lock-keywords-1)
 
 (defun coq-init-syntax-table ()
diff --git a/coq/ex-ssreflect.v b/coq/ex-ssreflect.v
new file mode 100644
index 00000000..54c4283a
--- /dev/null
+++ b/coq/ex-ssreflect.v
@@ -0,0 +1,136 @@
+(* An example of customization file for the hightlight of the Coq Mode *)
+
+(*Supposing you .emacs contains the following lines:
+
+(load-file "<proofgeneral-home>/generic/proof-site.el")
+(load-file "<location>/pg-ssr.el")
+
+And that the file my-tacs.el contains for instance:
+---
+
+(defcustom coq-user-tactics-db
+   '(("nat_congr" "ncongr"  "nat_congr" t "nat_congr")
+     ("nat_norm" "nnorm"  "nat_norm" t "nat_norm")
+     ("bool_congr" "bcongr"  "bool_congr" t "bool_congr")
+     ("prop_congr" "prcongr"  "prop_congr" t "prop_congr")
+     ("move" "m"  "move" t "move")
+     ("pose" "po"  "pose # := #" t "pose")
+     ("set" "set"  "set # := #" t "set")
+     ("have" "hv" "have # : #" t "have") 
+     ("congr" "con" "congr #" t "congr")
+     ("wlog" "wlog" "wlog : / #" t "wlog")
+     ("without loss" "wilog" "without loss #" t "without loss")
+     ("unlock" "unlock" "unlock #" t "unlock")
+     ("suffices" "suffices" "suffices # : #" t "suffices")
+     ("suff" "suff" "suff # : #" t "suff")
+) 
+   "Extended list of tactics, includings ssr and user defined ones")
+
+
+(defcustom coq-user-commands-db
+  '(("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits")
+    ("Hint View for" "hv" "Hint View for #" t "Hint\\s-+View\\s-+for")
+    ("inside" "ins" nil f "inside")
+    ("outside" "outs" nil f "outside")
+)
+   "Extended list of commands, includings ssr and user defined ones")
+
+(defcustom coq-user-tacticals-db
+  '(("last" "lst" nil t "last"))
+  "Extended list of tacticals, includings ssr and user defined ones")
+
+(defcustom coq-user-reserved-db
+  '("is" "nosimpl" "of")
+  "Extended list of keywords, includings ssr and user defined ones")
+
+(defcustom coq-user-solve-tactics-db
+  '(("done" nil "done" nil "done")
+    )
+   "Extended list of closing tactic(al)s, includings ssr and user defined ones")
+---
+Below is a sample script file coloured by this customised mode:
+
+*)
+
+
+
+Require Import ssreflect.
+Require Import ssrbool.
+Require Import ssrnat.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+
+Inductive mylist (A : Type) : Type := mynil | mycons of A & mylist A.
+
+(***************** The stack******************)
+
+Goal forall A B : Prop, A -> (A -> B) -> B.
+Proof. move=> A B Ha; exact. Qed.
+
+(***************** Bookkeeping **************)
+
+Lemma my_mulnI : forall x y, mult x y = muln x y.
+Proof. elim=> // m Hrec n /=; congr addn; done. Qed.
+
+
+(* Warning : corecion bool >-> Prop *)
+Lemma demo_bool : forall x y z: bool,
+  x && y -> z -> x && y && z.
+Proof. by move=> x y z -> ->. Qed.
+
+(* com + assoc *)
+Lemma my_addnCA : forall m n p, m + (n + p) = n + (m + p).
+Proof.  
+by move=> m n; elim: m => [|m Hrec] p; rewrite ?addSnnS -?addnS. Qed.
+
+(*** Rotation of subgoals *)
+Inductive test : nat -> Prop :=
+  C1 : forall n, test n | C2 : forall n, test n |
+  C3 : forall n, test n | C4 : forall n, test n.
+Goal forall n, test n -> True.
+move=> n t; case: t; last 1  [move=> k| move=> l]; last first.
+Admitted.
+
+(*** Selection of subgoals *)
+Goal forall n, test n -> True.
+move=> n t; case E: t; first 1 last.
+Admitted.
+
+
+(*** Forward chaining *)
+Lemma demo_fwd : forall x y : nat, x = y.
+Proof.
+move=> x y.
+ suff [H1 H2] : (x, y) = (x * 1, y + 0).
+Admitted.
+
+Lemma demo_fwd2 : forall x y : nat, x = y.
+Proof.
+move=> x y.
+  wlog : x  / x <= y.
+Admitted.
+
+
+
+Lemma rwtest1 : let x := 3 in x * 2 = 6.
+Proof. move=> x. rewrite /x //=. Qed.
+(* => unfold + simpl *)
+
+Lemma rwtest2 : forall x, 0 * x =  0.
+Proof. move=> x. rewrite -[0 * x]/0 //. Qed.
+(* => conversion *)
+
+Goal (forall t u, t + u = u + t) -> forall x y, x + y = y + x.
+Proof. by move=> H x y; rewrite (*[x + _ ]H *) [_ + y]H. Qed.
+(* => with patterns *)
+
+Goal (forall t u, t + u = u + t) -> 
+  forall x y, x + y + (y + x) = y + x.
+move=> H x y;  rewrite {2}(H y).
+Admitted.
+(* => occurrence selection *)
+
+