Update to Coq 8.0 syntax

3 files changed, 56 insertions, 26 deletions

diff --git a/coq/ex-module.v b/coq/ex-module.v
index af2e4a08..240d0ad1 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -30,7 +30,7 @@ Module M.
   End SIG.
   Lemma toto : O=O.
     Definition t:=nat.
-    Trivial.
+    trivial.
   Save.
   Module N:SIG.
     Definition T:=nat.
@@ -44,7 +44,7 @@ Print t.
 
 
 Definition t:O=O.
-  Trivial.
+  trivial.
 Save.
 
 
@@ -81,7 +81,7 @@ Module Type N'.
     
     
     Lemma titi : O=O.
-      Trivial.
+      trivial.
       Module Type K:=N'.
       Module N''':=M.
     Save.
diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v
index 21d94b93..ea6ef29c 100644
--- a/coq/example-x-symbols.v
+++ b/coq/example-x-symbols.v
@@ -1,4 +1,53 @@
-(* Grammar for symbols:
+(*
+    Example uses of X-Symbol symbols in Coq.
+    See end for syntax summary.
+
+    Pierre Courtieu
+
+    $Id$
+*)
+
+Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *)
+  match x with
+    | O => O        (* double arrow here *)
+    | S y => toto y (* double arrow here *)
+  end.
+
+Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *)
+ 
+
+(* this should appear like foo'a'1_B_3 where a and B are greek *)
+Variable foo'alpha'1_beta_3 : Set.  
+
+(* greek delta with a sub 1 and the same with super 1 *)
+Variable delta__1 delta^^1 : Set. 
+
+(* x with a+b subscripted and then superscripted *)
+Variable x_{a+b} x^{a+b} : Set. 
+
+(* no greek letter should appear on this next line! *)
+Variable philosophi   : Set.
+
+(* same here *)
+Variable aalpha alphaa : Set.
+
+
+(* _a where a is greek *)
+Variable _alpha : Set.
+
+(* a_ where a is greek *)
+Variable alpha_ : Set.
+
+
+alpha lhd rhd lambda forall exists exists exist 
+
+(* 
+Grammar for X-Symbols:
+
+  Symbols include sequences naming Greek letters ("Lambda", "lambda", etc),
+  connectives /\, \/, etc.  See the X-Symbol char table for details,
+  C-= C-=  (control with equals twice).
+
   a symbol is encoded only if 
    - preceded by _ or some space or some symbol
   **and**
@@ -8,7 +57,7 @@
 
    - a double _ introduces a subscript that ends at the first space
    - a double ^ introduces a superscript that ends at the first space
-  
+
    - a _ followed by { introduces a subscript
      expression that ends at the first }
    - a ^ followed by { introduces a superscript
@@ -16,22 +65,3 @@
  *)
 
 
-
-foo'alpha'1_beta_3  (* this should appear like foo'a'1_B_3 where a and B are greek *)
-delta__1 delta^^1          (* greek delta with a sub 1 and the same with super 1 *)
-x_{a+b} x^{a+b}         (* x with a+b subscripted and then superscripted *)
-philosophi   (* no greek letter should appear on this line *)
-aalpha alphaa (* no greek letter *)
-_alpha           (* _a where a is greek *)
-alpha_           (* a_ where a is greek *)
-
-
-
-Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *)
-  match x with
-    | O => O        (* double arrow here *)
-    | S y => toto y (* double arrow here *)
-  end.
-
-Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *)
- 
\ No newline at end of file
diff --git a/coq/example.v b/coq/example.v
index 6e88c5c8..95a9adac 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -5,9 +5,9 @@
 *)
 
 Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
-  intros A B H.
+  intros A B.
+  intros H.
   elim H.
-  intros.
   split.
   assumption.
   assumption.