modified the syntax for subscript in coq/pg

2 files changed, 31 insertions, 30 deletions

diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v
index ea6ef29c..5b48a2f5 100644
--- a/coq/example-x-symbols.v
+++ b/coq/example-x-symbols.v
@@ -1,6 +1,6 @@
 (*
     Example uses of X-Symbol symbols in Coq.
-    See end for syntax summary.
+    See README.
 
     Pierre Courtieu
 
@@ -19,11 +19,34 @@ 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.  
 
+Fixpoint pow (n m:nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => m * pow p m
+  end.
+
+Notation "a ,{ b }" := (a - b)
+  (at level 1, no associativity).
+
+Notation "a ^^ b" := (pow a b)
+  (at level 1, no associativity).
+
+Notation "a ^{ b }" := (pow a b)
+  (at level 1, no associativity).
+
+
+Variable delta:nat.
+
 (* greek delta with a sub 1 and the same with super 1 *)
-Variable delta__1 delta^^1 : Set. 
+Definition delta__1 := 0. 
+Definition delta__2 := delta^^1.
+Definition delta__3 := delta__2^{delta}.
 
+Parameter a b x:nat.
 (* x with a+b subscripted and then superscripted *)
-Variable x_{a+b} x^{a+b} : Set. 
+Definition x_a_b':= x^{a+b}. 
+Definition x_a_b := x,{a+b}.
+Definition x_a_b'' := x,{a+b}^{a*b}.
 
 (* no greek letter should appear on this next line! *)
 Variable philosophi   : Set.
@@ -38,30 +61,7 @@ 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**
-   - followed by _ or some space or some symbol
-
-  Grammar for sub/superscript: 
-
-   - 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
-     expression that ends at the first }
- *)
+Lemma gamma__neqn : forall n__i:nat, n__i=n__i.
 
 
+alpha lhd rhd lambda forall exists exists exist 
diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index a800e8bd..068def97 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -101,7 +101,7 @@ See language access `x-symbol-LANG-subscript-matcher'."
   :group 'x-symbol-coq
   :type 'function)
 
-(defcustom x-symbol-coq-font-lock-regexp "_{\\|__\\|\\^{\\|\\^\\^"
+(defcustom x-symbol-coq-font-lock-regexp ",{\\|__\\|\\^{\\|\\^\\^"
   "Regexp matching the start tag of Coq super- and subscripts."
   :group 'x-symbol-coq
   :type 'regexp)
@@ -130,7 +130,8 @@ or subscript tag."
       (while (re-search-forward x-symbol-coq-font-lock-regexp limit t)
         (setq open-beg (match-beginning 0)
               open-end (match-end 0)
-              script-type (if (eq (char-after (- open-end 2)) ?_)
+              script-type (if (or (eq (char-after (- open-end 2)) ?_)
+											 (eq (char-after (- open-end 2)) ?,))
                               'x-symbol-sub-face
 									 'x-symbol-sup-face))
         (if (or (eq (char-after (- open-end 1)) ?{)) ; if is spanning sup-/subscript