Remplacement de Syntactic Definition par Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 182 insertions, 129 deletions

diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 15f79158f3..ffb44d0d3d 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -13,41 +13,13 @@ Require Export Setoid.
 
 Set Implicit Arguments.
 
-Grammar ring formula : constr :=
-  formula_expr [ expr($p) ] -> [$p]
-| formula_eq [ expr($p) "==" expr($c) ] -> [ (Aequiv $p $c) ]
-
-with expr : constr :=
-  RIGHTA
-    expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
-  | expr_expr1 [ expr1($p) ] -> [$p]
-
-with expr1 : constr :=
-  RIGHTA
-    expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
-  | expr1_final [ final($p) ] -> [$p]
-
-with final : constr :=
-  final_var [ prim:var($id) ] -> [ $id ]
-| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ]
-| final_app [ "(" application($r) ")" ] -> [ $r ]
-| final_0 [ "0" ] -> [ Azero ]
-| final_1 [ "1" ] -> [ Aone ]
-| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ]
-
-with application : constr :=
-  LEFTA
-    app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
-  | app_tail [ expr($c1) ] -> [ $c1 ].
-
-Grammar constr constr0 :=
-  formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].
-
 Section Setoid_rings.
 
 Variable A : Type.
 Variable Aequiv : A -> A -> Prop.
 
+Infix "==" Aequiv (at level 5).
+
 Variable S : (Setoid_Theory A Aequiv).
 
 Add Setoid A Aequiv S.
@@ -59,12 +31,15 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Variable plus_morph : (a,a0,a1,a2:A)
- (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)).
-Variable mult_morph : (a,a0,a1,a2:A)
- (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)).
-Variable opp_morph : (a,a0:A)
- (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)).
+Infix "+" Aplus (at level 4).
+Infix "*" Amult (at level 3).
+Notation "0" := Azero.
+Notation "1" := Aone.
+Notation "- x" := (Aopp x) (at level 3).
+
+Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
+Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.
+Variable opp_morph : (a,a0:A) a == a0 -> -a == -a1.
 
 Add Morphism Aplus : Aplus_ext.
 Exact plus_morph.
@@ -81,16 +56,16 @@ Save.
 Section Theory_of_semi_setoid_rings.
 
 Record Semi_Setoid_Ring_Theory : Prop :=
-{ SSR_plus_sym  : (n,m:A) [| n + m == m + n |];
-  SSR_plus_assoc : (n,m,p:A) [| n + (m + p) == (n + m) + p |];
-  SSR_mult_sym : (n,m:A) [| n*m == m*n |];
-  SSR_mult_assoc : (n,m,p:A) [| n*(m*p) == (n*m)*p |];
-  SSR_plus_zero_left :(n:A) [| 0 + n == n|];
-  SSR_mult_one_left : (n:A) [| 1*n == n |];
-  SSR_mult_zero_left : (n:A) [| 0*n == 0 |];
-  SSR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
-  SSR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> (Aequiv m p);
-  SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y)
+{ SSR_plus_sym  : (n,m:A) n + m == m + n;
+  SSR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
+  SSR_mult_sym : (n,m:A) n*m == m*n;
+  SSR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
+  SSR_plus_zero_left :(n:A) 0 + n == n;
+  SSR_mult_one_left : (n:A) 1*n == n;
+  SSR_mult_zero_left : (n:A) 0*n == 0;
+  SSR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p;
+  SSR_plus_reg_left : (n,m,p:A)n + m == n + p -> m == p;
+  SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y
 }.
 
 Variable T : Semi_Setoid_Ring_Theory.
@@ -115,25 +90,25 @@ Hints Immediate equiv_sym.
 
 (* Lemmas whose form is x=y are also provided in form y=x because
   Auto does not symmetry *) 
-Lemma SSR_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
+Lemma SSR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
 Auto. Save.
 
-Lemma SSR_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
+Lemma SSR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
 Auto. Save.
 
-Lemma SSR_plus_zero_left2 : (n:A)[| n == 0 + n |].
+Lemma SSR_plus_zero_left2 : (n:A) n == 0 + n.
 Auto. Save.
 
-Lemma SSR_mult_one_left2 : (n:A)[| n == 1*n |].
+Lemma SSR_mult_one_left2 : (n:A) n == 1*n.
 Auto. Save.
 
-Lemma SSR_mult_zero_left2 : (n:A)[| 0 == 0*n |].
+Lemma SSR_mult_zero_left2 : (n:A) 0 == 0*n.
 Auto. Save.
 
-Lemma SSR_distr_left2 : (n,m,p:A)[| n*p + m*p  == (n + m)*p |].
+Lemma SSR_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
 Auto. Save.
 
-Lemma SSR_plus_permute : (n,m,p:A)[| n+(m+p) == m+(n+p) |].
+Lemma SSR_plus_permute : (n,m,p:A) n+(m+p) == m+(n+p).
 Intros.
 Rewrite (plus_assoc n m p).
 Rewrite (plus_sym n m).
@@ -141,7 +116,7 @@ Rewrite <- (plus_assoc m n p).
 Trivial.
 Save.
 
-Lemma SSR_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
+Lemma SSR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
 Intros.
 Rewrite (mult_assoc n m p).
 Rewrite (mult_sym n m).
@@ -151,7 +126,7 @@ Save.
 
 Hints Resolve SSR_plus_permute SSR_mult_permute.
 
-Lemma SSR_distr_right : (n,m,p:A) [| n*(m+p) == (n*m) + (n*p) |].
+Lemma SSR_distr_right : (n,m,p:A) n*(m+p) == (n*m) + (n*p).
 Intros.
 Rewrite (mult_sym n (Aplus m p)).
 Rewrite (mult_sym n m).
@@ -159,37 +134,37 @@ Rewrite (mult_sym n p).
 Auto.
 Save.
 
-Lemma SSR_distr_right2 : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p) |].
+Lemma SSR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p).
 Intros.
 Apply equiv_sym.
 Apply SSR_distr_right.
 Save.
 
-Lemma SSR_mult_zero_right : (n:A)[|  n*0 == 0|].
+Lemma SSR_mult_zero_right : (n:A) n*0 == 0.
 Intro; Rewrite (mult_sym n Azero); Auto.
 Save.
 
-Lemma SSR_mult_zero_right2 : (n:A)[| 0 == n*0 |].
+Lemma SSR_mult_zero_right2 : (n:A) 0 == n*0.
 Intro; Rewrite (mult_sym n Azero); Auto.
 Save.
 
-Lemma SSR_plus_zero_right :(n:A)[| n + 0 == n |].
+Lemma SSR_plus_zero_right :(n:A) n + 0 == n.
 Intro; Rewrite (plus_sym n Azero); Auto.
 Save.
 
-Lemma SSR_plus_zero_right2 :(n:A)[| n == n + 0 |].
+Lemma SSR_plus_zero_right2 :(n:A) n == n + 0.
 Intro; Rewrite (plus_sym n Azero); Auto.
 Save.
 
-Lemma SSR_mult_one_right : (n:A)[| n*1 == n |].
+Lemma SSR_mult_one_right : (n:A) n*1 == n.
 Intro; Rewrite (mult_sym n Aone); Auto.
 Save.
 
-Lemma SSR_mult_one_right2 : (n:A)[| n == n*1 |].
+Lemma SSR_mult_one_right2 : (n:A) n == n*1.
 Intro; Rewrite (mult_sym n Aone); Auto.
 Save.
 
-Lemma SSR_plus_reg_right : (n,m,p:A) [| m+n == p+n |] -> [| m==p |].
+Lemma SSR_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p.
 Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n).
 Intro; Apply plus_reg_left with n; Trivial.
 Save.
@@ -199,15 +174,15 @@ End Theory_of_semi_setoid_rings.
 Section Theory_of_setoid_rings.
 
 Record Setoid_Ring_Theory : Prop :=
-{ STh_plus_sym  : (n,m:A)[| n + m == m + n |];
-  STh_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-  STh_mult_sym : (n,m:A)[| n*m == m*n |];
-  STh_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
-  STh_plus_zero_left :(n:A)[| 0 + n == n|];
-  STh_mult_one_left : (n:A)[| 1*n == n |];
-  STh_opp_def : (n:A) [| n + (-n) == 0 |];
-  STh_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
-  STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv x y)
+{ STh_plus_sym  : (n,m:A) n + m == m + n;
+  STh_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
+  STh_mult_sym : (n,m:A) n*m == m*n;
+  STh_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
+  STh_plus_zero_left :(n:A) 0 + n == n;
+  STh_mult_one_left : (n:A) 1*n == n;
+  STh_opp_def : (n:A)  n + (-n) == 0;
+  STh_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p;
+  STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y
 }.
 
 Variable T : Setoid_Ring_Theory.
@@ -231,25 +206,25 @@ Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *)
 
-Lemma STh_mult_assoc2 : (n,m,p:A)[| (n * m) * p == n * (m * p) |].
+Lemma STh_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
 Auto. Save.
 
-Lemma STh_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |].
+Lemma STh_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
 Auto. Save.
 
-Lemma STh_plus_zero_left2 : (n:A)[| n == 0 + n |].
+Lemma STh_plus_zero_left2 : (n:A) n == 0 + n.
 Auto. Save.
 
-Lemma STh_mult_one_left2 : (n:A)[| n == 1*n |].
+Lemma STh_mult_one_left2 : (n:A) n == 1*n.
 Auto. Save.
 
-Lemma STh_distr_left2 : (n,m,p:A) [| n*p + m*p  == (n + m)*p |].
+Lemma STh_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
 Auto. Save.
 
-Lemma STh_opp_def2 : (n:A) [| 0 == n + (-n) |].
+Lemma STh_opp_def2 : (n:A) 0 == n + (-n).
 Auto. Save.
 
-Lemma STh_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |].
+Lemma STh_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p).
 Intros.
 Rewrite (plus_assoc n m p).
 Rewrite (plus_sym n m).
@@ -257,7 +232,7 @@ Rewrite <- (plus_assoc m n p).
 Trivial.
 Save.
 
-Lemma STh_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |].
+Lemma STh_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
 Intros.
 Rewrite (mult_assoc n m p).
 Rewrite (mult_sym n m).
@@ -267,7 +242,7 @@ Save.
 
 Hints Resolve STh_plus_permute STh_mult_permute.
 
-Lemma Saux1 : (a:A) [| a + a == a |] -> [| a == 0 |].
+Lemma Saux1 : (a:A)  a + a == a -> a == 0.
 Intros.
 Rewrite <- (plus_zero_left a).
 Rewrite (plus_sym Azero a).
@@ -277,7 +252,7 @@ Rewrite H.
 Apply opp_def.
 Save.
 
-Lemma STh_mult_zero_left :(n:A)[| 0*n == 0 |].
+Lemma STh_mult_zero_left :(n:A) 0*n == 0.
 Intros.
 Apply Saux1.
 Rewrite <- (distr_left Azero Azero n).
@@ -286,11 +261,11 @@ Trivial.
 Save.
 Hints Resolve STh_mult_zero_left.
 
-Lemma STh_mult_zero_left2 : (n:A)[| 0 == 0*n |].
+Lemma STh_mult_zero_left2 : (n:A) 0 == 0*n.
 Auto.
 Save.
 
-Lemma Saux2 : (x,y,z:A) [|x+y==0|] -> [|x+z==0|] -> (Aequiv y z). 
+Lemma Saux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y == z.
 Intros.
 Rewrite <- (plus_zero_left y).
 Rewrite <- H0.
@@ -301,7 +276,7 @@ Rewrite H.
 Auto.
 Save.
 
-Lemma STh_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |].
+Lemma STh_opp_mult_left : (x,y:A) -(x*y) == (-x)*y.
 Intros.
 Apply Saux2 with (Amult x y); Auto.
 Rewrite <- (distr_left x (Aopp x) y).
@@ -310,49 +285,49 @@ Auto.
 Save.
 Hints Resolve STh_opp_mult_left.
 
-Lemma STh_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y)  |].
+Lemma STh_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y) .
 Auto.
 Save.
 
-Lemma STh_mult_zero_right : (n:A)[| n*0 == 0|].
+Lemma STh_mult_zero_right : (n:A) n*0 == 0.
 Intro; Rewrite (mult_sym n Azero); Auto.
 Save.
 
-Lemma STh_mult_zero_right2 : (n:A)[| 0 == n*0 |].
+Lemma STh_mult_zero_right2 : (n:A) 0 == n*0.
 Intro; Rewrite (mult_sym n Azero); Auto.
 Save.
 
-Lemma STh_plus_zero_right :(n:A)[| n + 0 == n |].
+Lemma STh_plus_zero_right :(n:A) n + 0 == n.
 Intro; Rewrite (plus_sym n Azero); Auto.
 Save.
 
-Lemma STh_plus_zero_right2 :(n:A)[| n == n + 0 |].
+Lemma STh_plus_zero_right2 :(n:A) n == n + 0.
 Intro; Rewrite (plus_sym n Azero); Auto.
 Save.
 
-Lemma STh_mult_one_right : (n:A)[| n*1 == n |].
+Lemma STh_mult_one_right : (n:A) n*1 == n.
 Intro; Rewrite (mult_sym n Aone); Auto.
 Save.
 
-Lemma STh_mult_one_right2  : (n:A)[| n == n*1 |].
+Lemma STh_mult_one_right2  : (n:A) n == n*1.
 Intro; Rewrite (mult_sym n Aone); Auto.
 Save.
 
-Lemma STh_opp_mult_right : (x,y:A)[| -(x*y) == x*(-y) |].
+Lemma STh_opp_mult_right : (x,y:A) -(x*y) == x*(-y).
 Intros.
 Rewrite (mult_sym x y).
 Rewrite (mult_sym x (Aopp y)).
 Auto.
 Save.
 
-Lemma STh_opp_mult_right2 : (x,y:A)[| x*(-y) == -(x*y) |].
+Lemma STh_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y).
 Intros.
 Rewrite (mult_sym x y).
 Rewrite (mult_sym x (Aopp y)).
 Auto.
 Save.
 
-Lemma STh_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |].
+Lemma STh_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y).
 Intros.
 Apply Saux2 with (Aplus x y); Auto.
 Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)).
@@ -361,40 +336,40 @@ Rewrite (opp_def y); Rewrite (STh_plus_zero_right x).
 Rewrite (STh_opp_def2 x); Trivial.
 Save.
 
-Lemma STh_plus_permute_opp: (n,m,p:A)[| (-m)+(n+p) == n+((-m)+p) |].
+Lemma STh_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p).
 Auto.
 Save.
 
-Lemma STh_opp_opp : (n:A)[| -(-n) == n |].
+Lemma STh_opp_opp : (n:A) -(-n) == n.
 Intro.
 Apply Saux2 with (Aopp n); Auto.
 Rewrite (plus_sym (Aopp n) n); Auto.
 Save.
 Hints Resolve STh_opp_opp.
 
-Lemma STh_opp_opp2 : (n:A)[| n == -(-n) |].
+Lemma STh_opp_opp2 : (n:A) n == -(-n).
 Auto.
 Save.
 
-Lemma STh_mult_opp_opp : (x,y:A)[| (-x)*(-y) == x*y |].
+Lemma STh_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y.
 Intros.
 Rewrite (STh_opp_mult_left2 x (Aopp y)).
 Rewrite (STh_opp_mult_right2 x y).
 Trivial.
 Save.
 
-Lemma STh_mult_opp_opp2 : (x,y:A)[| x*y == (-x)*(-y) |].
+Lemma STh_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y).
 Intros.
 Apply equiv_sym.
 Apply STh_mult_opp_opp.
 Save.
 
-Lemma STh_opp_zero :[| -0 == 0 |].
+Lemma STh_opp_zero : -0 == 0.
 Rewrite <- (plus_zero_left (Aopp Azero)).
 Trivial.
 Save.
 
-Lemma STh_plus_reg_left : (n,m,p:A)[| n+m == n+p |] -> [|m==p|].
+Lemma STh_plus_reg_left : (n,m,p:A) n+m == n+p -> m==p.
 Intros.
 Rewrite <- (plus_zero_left m).
 Rewrite <- (plus_zero_left p).
@@ -405,14 +380,14 @@ Rewrite <- (plus_assoc (Aopp n) n p).
 Auto.
 Save.
 
-Lemma STh_plus_reg_right : (n,m,p:A)[| m+n == p+n |] -> [|m==p|].
+Lemma STh_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p.
 Intros.
 Apply STh_plus_reg_left with n.
 Rewrite (plus_sym n m); Rewrite (plus_sym n p);
 Assumption.
 Save.
 
-Lemma STh_distr_right : (n,m,p:A)[|n*(m+p) == (n*m)+(n*p)|].
+Lemma STh_distr_right : (n,m,p:A) n*(m+p) == (n*m)+(n*p).
 Intros.
 Rewrite (mult_sym n (Aplus m p)).
 Rewrite (mult_sym n m).
@@ -420,7 +395,7 @@ Rewrite (mult_sym n p).
 Trivial.
 Save.
 
-Lemma STh_distr_right2 : (n,m,p:A)(Aequiv (Aplus (Amult n m) (Amult n p)) (Amult n (Aplus m p))).
+Lemma STh_distr_right2 : (n,m,p:A) (n*m)+(n*p) == n*(m+p).
 Intros.
 Apply equiv_sym.
 Apply STh_distr_right.
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 126baea710..c125c4479d 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -56,10 +56,14 @@ exception Found of Gramext.g_assoc
 open Ppextend
 
 let admissible_assoc = function
-  | Gramext.LeftA, (Gramext.RightA | Gramext.NonA) -> false
-  | Gramext.RightA, Gramext.LeftA -> false
+  | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
+  | Gramext.RightA, Some Gramext.LeftA -> false
   | _ -> true
 
+let create_assoc = function
+  | None -> Gramext.RightA
+  | Some a -> a
+
 let find_position other assoc lev =
   let current = List.hd !level_stack in 
   match lev with
@@ -67,8 +71,7 @@ let find_position other assoc lev =
       level_stack := current :: !level_stack;
       None, (if other then assoc else None), None
   | Some n ->
-      let assoc = out_some assoc in
-      if n = 8 & assoc = Gramext.LeftA then 
+      if n = 8 & assoc = Some Gramext.LeftA then 
 	error "Left associativity not allowed at level 8";
       let after = ref (8,Gramext.RightA) in
       let rec add_level q = function
@@ -79,17 +82,18 @@ let find_position other assoc lev =
 	    if a = Gramext.LeftA then
 	      match l with
 		| (p,a)::_ as l' when p = n -> raise (Found a)
-		| _ -> after := pa; (n,assoc)::l'
+		| _ -> after := pa; (n,create_assoc assoc)::l'
 	    else
 	      (* This was not (p,LeftA) hence assoc is LeftA *)
-	      (after := q; (n,assoc)::l')
+	      (after := q; (n,create_assoc assoc)::l')
 	| l ->
-	    after := q; (n,assoc)::l
+	    after := q; (n,create_assoc assoc)::l
       in
       try
 	(* Create the entry *)
         let current = List.hd !level_stack in
         level_stack := add_level (8,Gramext.RightA) current :: !level_stack;
+	let assoc = create_assoc assoc in
         Some (Gramext.After (constr_level !after)),
 	Some assoc, Some (constr_level (n,assoc))
       with
@@ -138,8 +142,10 @@ let specify_name name e =
 
 open Names
 
-let make_act f pil =
-  let rec make env = function
+type 'a action_env = (identifier * 'a) list
+
+let make_act (f : loc -> constr_expr action_env -> constr_expr) pil =
+  let rec make (env : constr_expr action_env) = function
     | [] ->
 	Gramext.action (fun loc -> f loc env)
     | None :: tl -> (* parse a non-binding item *)
@@ -158,8 +164,9 @@ let make_act f pil =
 	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
 
-let make_cases_pattern_act f pil =
-  let rec make env = function
+let make_cases_pattern_act 
+  (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
+  let rec make (env : cases_pattern_expr action_env) = function
     | [] ->
 	Gramext.action (fun loc -> f loc env)
     | None :: tl -> (* parse a non-binding item *)
@@ -194,24 +201,95 @@ let symbol_of_prod_item univ assoc = function
       let eobj = build_prod_item univ assoc nt in
       (eobj, ovar)
 
+let coerce_to_id = function
+  | CRef (Ident (_,id)) -> id 
+  | c ->
+      user_err_loc (constr_loc c, "subst_rawconstr",
+        str"This expression should be a simple identifier")
+
+let coerce_to_ref = function
+  | CRef r -> r
+  | c ->
+      user_err_loc (constr_loc c, "subst_rawconstr",
+        str"This expression should be a simple reference")
+
+let subst_ref loc subst id =
+  try coerce_to_ref (List.assoc id subst) with Not_found -> Ident (loc,id)
+
+let subst_pat_id loc subst id =
+  try List.assoc id subst
+  with Not_found -> CPatAtom (loc,Some (Ident (loc,id)))
+
+let subst_id subst id =
+  try coerce_to_id (List.assoc id subst) with Not_found -> id
+
+let name_app f = function
+  | Name id -> Name (f id)
+  | Anonymous -> Anonymous
+
+let subst_cases_pattern_expr a loc subs =
+  let rec subst = function
+  | CPatAlias (_,p,x) -> CPatAlias (loc,subst p,x)
+    (* No subst in compound pattern ? *)
+  | CPatCstr (_,ref,pl) -> CPatCstr (loc,ref,List.map subst pl)
+  | CPatAtom (_,Some (Ident (_,id))) -> subst_pat_id loc subs id
+  | CPatAtom (_,x) -> CPatAtom (loc,x)
+  | CPatNumeral (_,n) -> CPatNumeral (loc,n)
+  | CPatDelimiters (_,key,p) -> CPatDelimiters (loc,key,subst p)
+  in subst a
+
+let subst_constr_expr a loc subs =
+  let rec subst = function
+  | CRef (Ident (_,id)) ->
+      (try List.assoc id subs with Not_found -> CRef (Ident (loc,id)))
+  (* Temporary: no robust treatment of substituted binders *)
+  | CLambdaN (_,[],c) -> subst c
+  | CLambdaN (_,([],t)::bl,c) -> subst (CLambdaN (loc,bl,c))
+  | CLambdaN (_,((_,na)::bl,t)::bll,c) -> 
+      let na = name_app (subst_id subs) na in
+      CLambdaN (loc,[[loc,na],subst t], subst (CLambdaN (loc,(bl,t)::bll,c)))
+  | CProdN (_,[],c) -> subst c
+  | CProdN (_,([],t)::bl,c) -> subst (CProdN (loc,bl,c))
+  | CProdN (_,((_,na)::bl,t)::bll,c) -> 
+      let na = name_app (subst_id subs) na in
+      CProdN (loc,[[loc,na],subst t], subst (CProdN (loc,(bl,t)::bll,c)))
+  | CLetIn (_,(_,na),b,c) ->
+      let na = name_app (subst_id subs) na in
+      CLetIn (loc,(loc,na),subst b,subst c)
+  | CArrow (_,a,b) -> CArrow (loc,subst a,subst b)
+  | CAppExpl (_,Ident (_,id),l) ->
+      CAppExpl (loc,subst_ref loc subs id,List.map subst l) 
+  | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) 
+  | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l)
+  | CCast (_,a,b) -> CCast (loc,subst a,subst b)
+  | CNotation (_,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,subst t)) l)
+  | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
+  | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x
+  | CCases (_,po,a,bl) ->
+      (* TODO: apply g on the binding variables in pat... *)
+      let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in
+      CCases (loc,option_app subst po,List.map subst a,bl)
+  | COrderedCase (_,s,po,a,bl) ->
+      COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
+  | CFix (_,id,dl) ->
+      CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
+  | CCoFix (_,id,dl) ->
+      CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
+  in subst a
+
 let make_rule univ assoc etyp rule =
   let pil = List.map (symbol_of_prod_item univ assoc) rule.gr_production in
   let (symbs,ntl) = List.split pil in
-  let f loc env = match rule.gr_action, env with
-    | AVar p, [p',a] when p=p' -> a
-    | AApp (AVar f,[AVar a]), [f',v;a',w] when f=f' & a=a' ->
-        CApp (loc,v,[w,None])
-    | AApp (AVar f,[AVar a]), [a',w;f',v] when f=f' & a=a' ->
-        CApp (loc,v,[w,None])
-    | pat,_ -> CGrammar (loc, pat, env) in
   let act = match etyp with
-    | ETPattern -> 
+    | ETPattern ->
         (* Ugly *)
         let f loc env = match rule.gr_action, env with
-          | AVar p, [p',a] when p=p' -> a
+          | CRef (Ident(_,p)), [p',a] when p=p' -> a
           | _ -> error "Unable to handle this grammar extension of pattern" in
-        make_cases_pattern_act f ntl
-    | _ -> make_act f ntl in
+	make_cases_pattern_act f ntl
+    | ETIdent | ETBigint | ETReference -> error "Cannot extend"
+    | ETConstr _ | ETOther _ -> 
+	make_act (subst_constr_expr rule.gr_action) ntl in
   (symbs, act)
 
 (* Rules of a level are entered in reverse order, so that the first rules
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 8d0dc0f5ca..3313827f1c 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -76,7 +76,7 @@ Grammar constr constr1 :=
 Definition equal := [A:Setoid]
    <[s:Setoid](Relation |s|)>let (S,R,e)=A in R.
 
-Grammar constr constr1 :=
+Grammar constr constr1 := NONA
  equal   [ constr0($c) "=" "%" "S" constr0($c2) ] -> 
          [ (equal ? $c $c2) ].
 
@@ -111,7 +111,7 @@ End Maps.
 
 Notation ap := (explicit_ap ? ?). 
 
-Grammar constr constr8 :=
+Grammar constr constr8 := RIGHTA
   map_setoid [ constr7($c1) "=>" constr8($c2) ] 
                  -> [ (Map_setoid $c1 $c2) ].