From 6a5f25529739c165007811bcafa40561fd21c348 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 6 Sep 2003 19:44:24 +0000
Subject: Mise en place possibilité de définitions locales dans les paramètres
 des records en v7 aussi

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4324 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d21c46cea8..193dd40fa6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -275,17 +275,14 @@ GEXTEND Gram
     [ [ fs = LIST0 record_field SEP ";" -> fs ] ]
   ;
   simple_params:
-    [ [ idl = LIST1 base_ident SEP ","; ":"; c = constr -> join_binders (idl, c)
-      | idl = LIST1 base_ident SEP "," -> join_binders (idl, evar_constr dummy_loc)
-    ] ]
+    [ [ nal = LIST1 name SEP ","; ":"; c = constr -> LocalRawAssum (nal, c)
+      | nal = LIST1 name SEP "," -> LocalRawAssum (nal, evar_constr loc) ] ]
   ;
   simple_binders:
-    [ [ "["; bll = LIST1 simple_params SEP ";"; "]" -> List.flatten bll ] ]
+    [ [ "["; bll = LIST1 vardecls SEP ";"; "]" -> bll ] ]
   ;
   ne_simple_binders_list:
-    [ [ bll = LIST1 simple_binders ->
-          List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
-            (List.flatten bll) ] ]
+    [ [ bll = LIST1 simple_binders -> (List.flatten bll) ] ]
   ;
   fix_params:
     [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
-- 
cgit v1.2.3