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

1 files changed, 5 insertions, 5 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 *)