Changement/extension dans les noms de parseurs de Grammar

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

6 files changed, 25 insertions, 230 deletions

diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index 327f23a64..af673b097 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Grammar vernac vernac : Ast :=
+Grammar vernac vernac : ast :=
   omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
 | omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
 | omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")]
@@ -21,7 +21,7 @@ Grammar vernac vernac : Ast :=
 | omega_set  [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)].
 
 
-Grammar tactic simple_tactic : Ast :=
+Grammar tactic simple_tactic : ast :=
   omega [ "Omega" ] -> [(Omega)].
 
 Syntax tactic level 0:
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index abde178e1..e7c995cf3 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -79,7 +79,7 @@ Implicit Arguments Off.
 
 Declare ML Module "quote".
 
-Grammar tactic simple_tactic : Ast := 
+Grammar tactic simple_tactic : ast := 
   quote [ "Quote" identarg($f) ] -> [(Quote $f)]
 | quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] ->  
                    [ (Quote $f ($LIST $lc)) ].
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 9045eab5f..81b2077a4 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -9,14 +9,14 @@ Require Export Ring_abstract.
 
 Declare ML Module "ring".
 
-Grammar tactic simple_tactic : Ast :=
+Grammar tactic simple_tactic : ast :=
   ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
 
 Syntax tactic level 0:
   ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] 
 | ring_e [ << (Ring) >> ] -> ["Ring"].
  
-Grammar vernac vernac : Ast := 
+Grammar vernac vernac : ast := 
   addring [ "Add" "Ring" 
       	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
       	     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 6bb1f5aa9..60fa01ff1 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -448,210 +448,4 @@ Tactic Definition Solve1 :=
     [Rewrite H; Simpl; Auto
     |Simpl in H0; Rewrite H0; Auto ].
 
-Lemma signed_sum_merge_ok : (x,y:signed_sum)
-  (interp_sacs (signed_sum_merge x y))
-  ==(Aplus (interp_sacs x) (interp_sacs y)).
-
-  Induction x.
-  Intro; Simpl; Auto.
-
-  Induction y; Intros.
-
-  Auto.
-
-  Solve1.
-
-  Simpl; Generalize (varlist_eq_prop v v0).
-  Elim (varlist_eq v v0); Simpl.
-
-  Intro Heq; Rewrite (Heq I).
-  Rewrite H.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite (Th_plus_permute T). 
-  Repeat Rewrite (Th_plus_assoc T).
-  Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v0))
-                         (interp_vl Amult Aone Azero vm v0)).
-  Rewrite (Th_opp_def T).
-  Rewrite (Th_plus_zero_left T).
-  Reflexivity.
-
-  Solve1.
-
-  Induction y; Intros.
-
-  Auto.
-
-  Simpl; Generalize (varlist_eq_prop v v0).
-  Elim (varlist_eq v v0); Simpl.
-
-  Intro Heq; Rewrite (Heq I).
-  Rewrite H.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite (Th_plus_permute T). 
-  Repeat Rewrite (Th_plus_assoc T).
-  Rewrite (Th_opp_def T).
-  Rewrite (Th_plus_zero_left T).
-  Reflexivity.
-
-  Solve1.
-
-  Solve1.
-
-Save.
-
-Tactic Definition Solve2 :=
- 	Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok;
-  	[ Auto
-  	| Rewrite H; Auto ].
-
-Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum)
-	(interp_sacs (plus_varlist_insert l s)) 
-	== (Aplus (interp_vl  Amult Aone Azero vm l) (interp_sacs s)).
-Proof.
-
-  Induction s.
-  Trivial.
-
-  Simpl; Intros.
-  Solve2.
-
-  Simpl; Intros.
-  Generalize (varlist_eq_prop l v).
-  Elim (varlist_eq l v); Simpl.
-
-  Intro Heq; Rewrite (Heq I).
-  Repeat Rewrite isacs_aux_ok.
-  Repeat Rewrite (Th_plus_assoc T).
-  Rewrite (Th_opp_def T).
-  Rewrite (Th_plus_zero_left T).
-  Reflexivity.
-
-  Solve2.
-
-Save.
-
-Lemma minus_varlist_insert_ok : (l:varlist)(s:signed_sum)
-	(interp_sacs (minus_varlist_insert l s)) 
-	== (Aplus (Aopp (interp_vl  Amult Aone Azero vm l)) (interp_sacs s)).
-Proof.
-
-  Induction s.
-  Trivial.
-
-  Simpl; Intros.
-  Generalize (varlist_eq_prop l v).
-  Elim (varlist_eq l v); Simpl.
-
-  Intro Heq; Rewrite (Heq I).
-  Repeat Rewrite isacs_aux_ok.
-  Repeat Rewrite (Th_plus_assoc T).
-  Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v))
-         (interp_vl Amult Aone Azero vm v)).
-  Rewrite (Th_opp_def T).
-  Auto.
-
-  Simpl; Intros.
-  Solve2.
-
-  Simpl; Intros; Solve2.
-
-Save.
-
-Lemma plus_sum_scalar_ok : (l:varlist)(s:signed_sum)
-	(interp_sacs (plus_sum_scalar l s)) 
-	== (Amult (interp_vl  Amult Aone Azero vm l) (interp_sacs s)).
-Proof.
-
-  Induction s.
-  Trivial.
-
-  Simpl; Intros.
-  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite H.
-  Auto.
-
-  Simpl; Intros.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  Rewrite H.
-  Rewrite (Th_distr_right T).
-  Rewrite <- (Th_opp_mult_right T).
-  Reflexivity.
-
-Save.
-
-Lemma minus_sum_scalar_ok : (l:varlist)(s:signed_sum)
-	(interp_sacs (minus_sum_scalar l s)) 
-	== (Aopp (Amult (interp_vl  Amult Aone Azero vm l) (interp_sacs s))).
-Proof.
-
-  Induction s; Simpl; Intros.
-
-  Rewrite (Th_mult_zero_right T); Symmetry; Apply (Th_opp_zero T).
-
-  Simpl; Intros.
-  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite H.
-  Rewrite (Th_distr_right T).
-  Rewrite (Th_plus_opp_opp T).
-  Reflexivity.
-
-  Simpl; Intros.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  Rewrite H.
-  Rewrite (Th_distr_right T).
-  Rewrite <- (Th_opp_mult_right T).
-  Rewrite <- (Th_plus_opp_opp T).
-  Rewrite (Th_opp_opp T).
-  Reflexivity.
-
-Save.
-
-Lemma signed_sum_prod_ok : (x,y:signed_sum)
-	(interp_sacs (signed_sum_prod x y)) ==
-		(Amult (interp_sacs x) (interp_sacs y)).
-Proof.
-
-  Induction x.
-
-  Simpl; EAuto 1.
-
-  Intros; Simpl.
-  Rewrite signed_sum_merge_ok.
-  Rewrite plus_sum_scalar_ok.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite H.
-  Auto.
-
-  Intros; Simpl.
-  Repeat Rewrite isacs_aux_ok.
-  Rewrite signed_sum_merge_ok.
-  Rewrite minus_sum_scalar_ok.
-  Rewrite H.
-  Rewrite (Th_distr_left T).
-  Rewrite (Th_opp_mult_left T).
-  Reflexivity.
-
-Save.
-
-Theorem apolynomial_normalize_ok : (p:apolynomial)
-	(interp_sacs (apolynomial_normalize p))==(interp_ap p).
-Proof.
-  Induction p; Simpl; Auto 1.
-  Intros.
-    Rewrite signed_sum_merge_ok.
-    Rewrite H; Rewrite H0; Reflexivity.
-  Intros.
-    Rewrite signed_sum_prod_ok.
-    Rewrite H; Rewrite H0; Reflexivity.
-  Intros.
-    Rewrite minus_sum_scalar_ok.
-    Simpl. 
-    Rewrite (Th_mult_one_left T).
-    Rewrite H; Reflexivity.
-Save.  
-
 End abstract_rings.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index adf55b500..2901942ef 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -5,34 +5,35 @@ Require Export Bool.
 
 Implicit Arguments On.
 
-Grammar ring formula :=
+Grammar ring formula : constr :=
   formula_expr [ expr($p) ] -> [$p]
-| formula_eq [ expr($p) "==" expr($c) ] -> [<<(eqT A $p $c)>>]
-with expr :=
+| formula_eq [ expr($p) "==" expr($c) ] -> [ (eqT A $p $c) ]
+
+with expr : constr :=
   RIGHTA
-    expr_plus [ expr($p) "+" expr($c) ] -> [<<(Aplus $p $c)>>]
+    expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
   | expr_expr1 [ expr1($p) ] -> [$p]
 
-with expr1 :=
+with expr1 : constr :=
   RIGHTA
-    expr1_plus [ expr1($p) "*" expr1($c) ] -> [<<(Amult $p $c)>>]
+    expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
   | expr1_final [ final($p) ] -> [$p]
 
-with final :=
-  final_var [ prim:var($id) ] -> [$id]
-| final_command [ "[" command:command($c) "]" ] -> [$c]
-| final_app [ "(" application($r) ")" ] -> [$r]
-| final_0 [ "0" ] -> [<<Azero>>]
-| final_1 [ "1" ] -> [<<Aone>>]
-| final_uminus [ "-" expr($c) ] -> [<<(Aopp $c)>>]
+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 :=
+with application : constr :=
   LEFTA
-    app_cons [ application($p) application($c1) ] -> [<<($p $c1)>>]
-  | app_tail [ expr($c1) ] -> [$c1].
+    app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
+  | app_tail [ expr($c1) ] -> [ $c1 ].
 
-Grammar command command0 :=
-  formula_in_command [ "[" "|" ring:formula($c) "|" "]" ] -> [$c].
+Grammar constr constr0 :=
+  formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].
 
 Section Theory_of_semi_rings.
 
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index 0c82ae669..edd50e79d 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -10,7 +10,7 @@
 
 Declare ML Module "xml" "xmlcommand" "xmlentries".
 
-Grammar vernac vernac : Ast :=
+Grammar vernac vernac : ast :=
   xml_print [ "Print" "XML" identarg($id) "." ] ->
                [(Print $id)]