Do a second pass on the treatment of user-given implicit arguments. Now

works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections. 
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.


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

1 files changed, 28 insertions, 9 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 68389c54a..423ade8b6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -103,13 +103,16 @@ let impl_ident =
   Gram.Entry.of_parser "impl_ident"
     (fun strm ->
       match Stream.npeek 1 strm with
-	| [("IDENT",("wf"|"struct"|"measure"))] ->
-	    raise Stream.Failure
-	| [("IDENT",s)] -> 
-	    Stream.junk strm;
-            Names.id_of_string s
+	| [(_,"{")] -> 
+	    (match Stream.npeek 2 strm with
+	      | [_;("IDENT",("wf"|"struct"|"measure"))] ->
+		  raise Stream.Failure
+	      | [_;("IDENT",s)] -> 
+		  Stream.junk strm; Stream.junk strm;
+		  Names.id_of_string s
+	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
-
+    
 let ident_eq =
   Gram.Entry.of_parser "ident_eq"
     (fun strm ->
@@ -356,10 +359,26 @@ GEXTEND Gram
 	  ctx @ bl
     | cl = LIST0 binder_let -> cl ] ]
   ;
+  binder_assum:
+    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
+    | idl=LIST1 name; ":"; c=lconstr; "}" ->
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
+    | idl=LIST1 name; "}" ->
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)))
+    | ":"; c=lconstr; "}" ->
+	(fun id -> LocalRawAssum ([id],Default Implicit,c))
+    ] ]
+  ;
+  fixannot:
+    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
+    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
+    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
+    ] ]
+  ;
   binders_let_fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> [], (Some id, CStructRec)
-    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> [], (id, CWfRec rel)
-    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> [], (id, CMeasureRec rel)
+    [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot -> 
+	(assum (loc, Name id) :: fst bl), snd bl
+    | f = fixannot -> [], f
     | b = binder_let; bl = binders_let_fixannot -> 
 	b :: fst bl, snd bl
     | -> [], (None, CStructRec)