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

3 files changed, 31 insertions, 30 deletions

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 520c988d24..fb6476e7ea 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -7,18 +7,18 @@ Require Export Datatypes.
 
 Grammar constr constr1 :=
   pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) ","
-    lconstr($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
+    lconstr($c4) ")" ] -> [ (pair $l1 $c2 $c3 $c4) ]
 | fst_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "("
-    lconstr($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
+    lconstr($l) ")" ] -> [ (fst $l1 $c2 $l) ]
 | snd_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "("
-    lconstr($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
+    lconstr($l) ")" ] -> [ (snd $l1 $c2 $l) ]
 
 with constr0 :=
   pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
-         [<<(pair ? ? $lc1 $lc2)>>]
+         [ (pair ? ? $lc1 $lc2) ]
 
 with constr3 :=
-  prod [ constr2($c1) "*" constr3($c2) ] -> [<<(prod $c1 $c2)>>].
+  prod [ constr2($c1) "*" constr3($c2) ] -> [ (prod $c1 $c2) ].
 
 (* Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 50bed88279..57b76e0176 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -7,44 +7,44 @@ Require Export Logic.
 
 Grammar constr constr1 :=
   conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) ","
-        constr($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
+        constr($c4) "}" ] -> [ (conj $l1 $c2 $c3 $c4) ]
 | proj1 [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "{"
-        lconstr($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
+        lconstr($l) "}" ] -> [ (proj1 $l1 $c2 $l) ]
 | proj2 [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "{"
-        lconstr($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
+        lconstr($l) "}" ] -> [ (proj2 $l1 $c2 $l) ]
 | IF [ "either" constr($c) "and_then" constr($t) "or_else" constr($e) ] ->
-       [<<(IF $c $t $e)>>]
+       [ (IF $c $t $e) ]
 | all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] ->
-       [<<(all $l1 $l2)>>]
+       [ (all $l1 $l2) ]
 | eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
-            [<<(eq $l1 $c1 $c2)>>]
-| eq_impl [ constr0($c) "=" constr0($c2) ] -> [<<(eq ? $c $c2)>>]
+            [ (eq $l1 $c1 $c2) ]
+| eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq ? $c $c2) ]
 
 with constr2 :=
-  not [ "~" constr2($c) ] -> [<<(not $c)>>]
+  not [ "~" constr2($c) ] -> [ (not $c) ]
 
 with constr6 :=
-  and [ constr5($c1) "/\\" constr6($c2) ] -> [<<(and $c1 $c2)>>]
+  and [ constr5($c1) "/\\" constr6($c2) ] -> [ (and $c1 $c2) ]
 
 with constr7 :=
-  or [ constr6($c1) "\\/" constr7($c2) ] -> [<<(or $c1 $c2)>>]
+  or [ constr6($c1) "\\/" constr7($c2) ] -> [ (or $c1 $c2) ]
 
 with constr8 :=
-  iff [ constr7($c1) "<->" constr8($c2) ] -> [<<(iff $c1 $c2)>>]
+  iff [ constr7($c1) "<->" constr8($c2) ] -> [ (iff $c1 $c2) ]
 
 with constr10 :=
   allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
-                          -> [<<(all $t [$x : $t]$p)>>]
+                          -> [ (all $t [$x : $t]$p) ]
 | allimplicit [ "ALL" ident($x) "|" constr($p) ]
-                          -> [<<(all ? [$x]$p)>>]
+                          -> [ (all ? [$x]$p) ]
 | exexplicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) ]
-                          -> [<<(ex $t [$v : $t]$c1)>>]
+                          -> [ (ex $t [$v : $t]$c1) ]
 | eximplicit [ "EX" ident($v) "|" constr($c1) ] 
-                          -> [<<(ex ? [$v]$c1)>>]
+                          -> [ (ex ? [$v]$c1) ]
 | ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&"
-           constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : $t]$c2)>>]
+           constr($c2) ] -> [ (ex2 $t [$v : $t]$c1 [$v : $t]$c2) ]
 | ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
-           constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
+           constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ].
 
 
 (* Pretty-printing of things in Logic.v *)
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8b467fe13f..a3a69c3100 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,20 +8,21 @@ Require Export Specif.
 
 Grammar constr constr1 :=
   sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
-       -> [<<(sig $c1 [$lc : $c1]$c2)>>]
+       -> [ (sig $c1 [$lc : $c1]$c2) ]
 
 | sig2 [ "{" lconstr($lc) ":" lconstr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [<<(sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
+       -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
 
 | sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
-       -> [<<(sigS $c1 [$lc : $c1]$c2)>>]
+       -> [ (sigS $c1 [$lc : $c1]$c2) ]
 
 | sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [<<(sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
+       -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-| squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
+Grammar constr constr1: Ast :=
+  squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
 
 Grammar constr lassoc_constr4 :=
   squash_sum
@@ -29,10 +30,10 @@ Grammar constr lassoc_constr4 :=
       case [$c2] of
         (SQUASH $T2) ->
             case [$c1] of
-              (SQUASH $T1) -> [<<(sumbool $T1 $T2)>>] (* {T1}+{T2} *)
-            | $_           -> [<<(sumor $c1 $T2)>>]   (* c1+{T2} *)
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
             esac
-      | $_           -> [<<(sum $c1 $c2)>>]           (* c1+c2 *)
+      | $_           -> [ (sum $c1 $c2) ]           (* c1+c2 *)
       esac.
 
 (* Pretty-printing of things in Specif.v *)