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

2 files changed, 48 insertions, 8 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 156d155667..49b719bdb5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1144,17 +1144,36 @@ let intern_pattern env patt =
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
+type manual_implicits = (explicitation * (bool * bool)) list
+
+let implicits_of_rawterm l = 
+  let rec aux i c = 
+    match c with
+	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
+	  let rest = aux (succ i) b in
+	    if bk = Implicit then
+	      let name =
+		match na with
+		    Name id -> Some id
+		  | Anonymous -> None
+	      in
+		(ExplByPos (i, name), (true, true)) :: rest
+	    else rest
+      | RLetIn (loc, na, t, b) -> aux i b
+      | _ -> []
+  in aux 1 l
+
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env 
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  Default.understand_gen kind sigma env 
-    (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c)
+  let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+    Default.understand_gen kind sigma env c
 
 let interp_constr sigma env c =
-  interp_gen (OfType None) sigma env c 
+  interp_gen (OfType None) sigma env c
 
 let interp_type sigma env ?(impls=([],[])) c =
   interp_gen IsType sigma env ~impls c
@@ -1168,9 +1187,20 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
+let interp_constr_evars_gen_impls evdref env ?(impls=([],[])) kind c =
+  let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+  let imps = implicits_of_rawterm c in
+    Default.understand_tcc_evars evdref env kind c, imps
+
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
-  Default.understand_tcc_evars evdref env kind
-    (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+  let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+    Default.understand_tcc_evars evdref env kind c
+      
+let interp_casted_constr_evars_impls evdref env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen_impls evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls evdref env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls evdref env IsType ~impls c
 
 let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f4272a2b19..9f3a815ee0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,6 +45,8 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
+type manual_implicits = (explicitation * (bool * bool)) list
+
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 (*s Internalisation performs interpretation of global names and notations *)
@@ -74,14 +76,22 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env -> 
   constr_expr -> constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
-  constr_expr -> types -> constr
-
 val interp_type : evar_map -> env -> ?impls:full_implicits_env -> 
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types -> constr
+
+(* Accepting evars and giving back the manual implicits in addition. *)
+
+val interp_casted_constr_evars_impls : evar_defs ref -> env -> 
+  ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+
+val interp_type_evars_impls : evar_defs ref -> env -> ?impls:full_implicits_env ->
+  constr_expr -> types * manual_implicits
+
 val interp_casted_constr_evars : evar_defs ref -> env -> 
   ?impls:full_implicits_env -> constr_expr -> types -> constr