Mise en place possibilité de définitions locales dans les paramètres des records

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 4 insertions, 21 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 21906628cd..d21c46cea8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -222,9 +222,6 @@ GEXTEND Gram
   oneind:
     [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
         ntn = OPT decl_notation ; ":="; lc = constructor_list ->
-	  let indpar = 
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
-	      indpar in
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
@@ -286,7 +283,9 @@ GEXTEND Gram
     [ [ "["; bll = LIST1 simple_params SEP ";"; "]" -> List.flatten bll ] ]
   ;
   ne_simple_binders_list:
-    [ [ bll = LIST1 simple_binders -> List.flatten bll ] ]
+    [ [ bll = LIST1 simple_binders ->
+          List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
+            (List.flatten bll) ] ]
   ;
   fix_params:
     [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
@@ -306,9 +305,6 @@ GEXTEND Gram
   gallina_ext:
     [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
         indl = block_old_style ->
-	  let bl = 
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) bl
-	  in
 	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
       | b = record_token; oc = opt_coercion; name = base_ident;
@@ -327,9 +323,6 @@ GEXTEND Gram
       | IDENT "Scheme"; l = schemes -> VernacScheme l
       | f = finite_token; s = csort; id = base_ident;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
-	  let indpar =
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
-	      indpar in
           VernacInductive (f,[id,None,indpar,s,lc]) ] ]
   ;
   csort:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 3c1fad5d18..34bdbbb8cc 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -120,7 +120,7 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = base_ident;
-        ps = LIST0 simple_binder; ":";
+        ps = LIST0 binder_let; ":";
 	s = lconstr; ":="; cstr = OPT base_ident; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
@@ -250,9 +250,6 @@ GEXTEND Gram
   ;
   (* Various Binders *)
   (* ... without coercions *)
-  simple_binder:
-    [ [ b = simple_binder_coe -> no_coercion loc b ] ]
-  ;
   binder_nodef:
     [ [ b = binder_let ->
       (match b with
@@ -283,13 +280,6 @@ GEXTEND Gram
     [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr -> 
         (oc,(idl,c)) ] ]
   ;
-  simple_binder_coe:
-    [ [ id=base_ident -> (false,(id,CHole loc))
-      | "("; id = base_ident; ")" -> (false,(id,CHole loc))
-      | "("; id = base_ident; oc = of_type_with_opt_coercion;
-             t = lconstr; ")" ->
-         (oc,(id,t)) ] ]
-  ;
   constructor:
     [ [ id = base_ident; l = LIST0 binder_let; 
         coe = of_type_with_opt_coercion; c = lconstr ->