Plus de piquants dans les actions des grammaires; nom de la grammaire pris comme parseur par defaut; le type List devient AstList

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

4 files changed, 26 insertions, 26 deletions

diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index c03334aebd..f56d9aadc1 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -13,7 +13,7 @@
 (*                                 Prolog.v                                 *)
 (****************************************************************************)
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   eapply [ "EApply" constrarg_binding_list($cl) ]
       -> [(EApplyWithBindings ($LIST $cl))]
 | eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 1cbf506270..95739e8388 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -3,41 +3,41 @@
 
 Declare ML Module "equality".
 
-Grammar vernac orient_rule:=
-   lr ["LR"] -> ["LR"]
-  |rl ["RL"] -> ["RL"]
-with rule_list: List :=
+Grammar vernac orient_rule: Ast :=
+   lr ["LR"] -> [ "LR" ]
+  |rl ["RL"] -> [ "RL" ]
+with rule_list: AstList :=
    single_rlt [ constrarg($com) orient_rule($ort) ] ->
-     [(VERNACARGLIST $com $ort)]
+     [ (VERNACARGLIST $com $ort) ]
   |recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] ->
-    [(VERNACARGLIST $com $ort) ($LIST $tail)]
-with base_list: List :=
+    [ (VERNACARGLIST $com $ort) ($LIST $tail) ]
+with base_list: AstList :=
    single_blt [identarg($rbase) "[" rule_list($rlt) "]"] ->
-     [(VERNACARGLIST $rbase ($LIST $rlt))]
+     [ (VERNACARGLIST $rbase ($LIST $rlt)) ]
   |recursive_blt [identarg($rbase) "[" rule_list($rlt) "]"
     base_list($blt)] ->
-    [(VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt)]
-with vernac:=
+    [ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ]
+with vernac: Ast :=
    addrule ["HintRewrite" base_list($blt) "."] ->
-     [(HintRewrite ($LIST $blt))].
+     [ (HintRewrite ($LIST $blt)) ].
 
-Grammar tactic list_tactics: List :=
+Grammar tactic list_tactics: AstList :=
    single_lt [tactic($tac)] -> [$tac]
   |recursive_lt [tactic($tac) "|" list_tactics($tail)] ->
-    [$tac ($LIST $tail)]
+    [ $tac ($LIST $tail) ]
 
-with step_largs: List :=
+with step_largs: AstList :=
    nil_step [] -> []
   |solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))]
   |use_step ["with" "Use"] -> [(REDEXP (Use))]
   |all_step ["with" "All"] -> [(REDEXP (All))]
 
-with rest_largs: List :=
+with rest_largs: AstList :=
    nil_rest [] -> []
   |solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))]
   |cond_rest ["with" "Cond"] -> [(REDEXP (Cond))]
 
-with autorew_largs: List :=
+with autorew_largs: AstList :=
    step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] ->
     [(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)]
   |rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] ->
@@ -45,30 +45,30 @@ with autorew_largs: List :=
   |depth_arg ["Depth" "=" numarg($dth)] ->
     [(REDEXP (Depth $dth))]
 
-with list_args_autorew: List :=
+with list_args_autorew: AstList :=
    nil_laa [] -> []
   |recursive_laa [autorew_largs($largs) list_args_autorew($laa)] ->
     [($LIST $largs) ($LIST $laa)]
 
-with hintbase_list: List :=
+with hintbase_list: AstList :=
   nil_hintbase [] -> []
 | base_by_name [identarg($id) hintbase_list($tail)] -> 
        [ (REDEXP (ByName $id)) ($LIST $tail)]
 | explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] -> 
        [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
 
-with hintbase: List := 
+with hintbase: AstList := 
   onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
 | onehint_rl  [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
 | conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
 | conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
 
-with simple_tactic := 
+with simple_tactic: Ast := 
  AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
   list_args_autorew($laa)] ->
   [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
 
 | deqhyp   [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 544232c400..d2df140e5f 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -26,7 +26,7 @@ Syntax tactic level 0:
 | inversion_clear  [(INVCOM InversionClear)] -> [ "Inversion_clear" ].
 
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
 | inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
       -> [(InvIn $ic $id ($LIST $l))]
@@ -48,13 +48,13 @@ Grammar tactic simple_tactic :=
           Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))]
         esac
 
-with inversion_com :=
+with inversion_com: Ast :=
   simple_inv    [ "Simple" "Inversion" ] -> [ HalfInversion ]
 | inversion_com [ "Inversion" ] -> [ Inversion ]
 | inv_clear     [ "Inversion_clear" ] -> [ InversionClear ].
 
 
-Grammar vernac vernac :=
+Grammar vernac vernac: Ast :=
   der_inv_clr [ "Derive" "Inversion_clear"  identarg($na) identarg($id) "." ]
                -> [(MakeInversionLemmaFromHyp 1 $na $id)]
 
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index 2f7cbb0eac..40a4a048b6 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -3,7 +3,7 @@
 
 Declare ML Module "Tauto".
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic: Ast :=
   tauto [ "Tauto" ] -> [(Tauto)]
 | intuition [ "Intuition" ] -> [(Intuition)].