From 143e230bc7073b4623aa7e2e51bd8cde3ea6bbbf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Feb 2007 16:19:30 +0000
Subject: Factorisation de la règle Constr.binder dans g_subtac.ml pour éviter
 de cacher l'instance de la règle figurant dans g_constr (report révision 9588
 de 8.1 vers trunk)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9589 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/g_subtac.ml4 | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 337cc09fc1..933ea94b31 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -67,10 +67,12 @@ GEXTEND Gram
 
   Constr.binder:
     [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
-	    ([id], typ) ] ];
-
-
+          ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+      | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
+          ([id],c)
+      | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
+          (id::lid,c)
+    ] ];
 
   END
 
-- 
cgit v1.2.3