From 133a519c08d9ce525901e8800b021eff6ed72cf0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 Oct 2002 11:16:09 +0000
Subject: Bugs dans la factorisation des règles de parsing de "{ ... } * ..."

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3156 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/SpecifSyntax.v | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index b64278f7dc..38e11e8f3e 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -15,34 +15,35 @@ Require Specif.
 
 (* To accept {x:A|P}*B without parentheses *)
 Grammar constr constr6 :=
-  sig [ "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" "*" constr6($c) ]
+  sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}"
+            "*" constr6($c) ]
        -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
 
-| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
+| sig2prod [ "{" lconstr($lc) ":" lconstr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ]
        -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
 
-| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
+| sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
          "*" constr6($c)]
        -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
 
-| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
+| sigS2prod [ "{" lconstr($lc) ":" lconstr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr6($c) ]
        -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
 
 (* To factor with {A}+{B} *)
 Grammar constr constr6 :=
-  sig [ "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ]
+  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [ (sig $c1 [$lc : $c1]$c2) ]
 
-| sig2 [ "{" lconstr($lc) ":" constr($c1)
+| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
            "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
 
-| sigS [ "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
+| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
        -> [ (sigS $c1 [$lc : $c1]$c2) ]
 
-| sigS2 [ "{" lconstr($lc) ":" constr($c1)
+| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
              "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
 
-- 
cgit v1.2.3