Finish fix in command where we still lost information on what was a type

and needed coercions. Change API of interp_constr_evars to get an
optional evar_defs ref argument. Makes Algebra compile again (at least).


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

3 files changed, 25 insertions, 24 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 49b719bdb5..ee245450b4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1187,7 +1187,8 @@ 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 interp_constr_evars_gen_impls ?(evdref=ref Evd.empty_evar_defs) 
+    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
@@ -1196,11 +1197,15 @@ let interp_constr_evars_gen evdref env ?(impls=([],[])) kind 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_casted_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs)
+    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_type_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ~evdref env IsType ~impls c
+
+let interp_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ~evdref env (OfType None) ~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 9f3a815ee0..f81b2ccd16 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -86,12 +86,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
 
 (* Accepting evars and giving back the manual implicits in addition. *)
 
-val interp_casted_constr_evars_impls : evar_defs ref -> env -> 
+val interp_casted_constr_evars_impls : ?evdref:(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 ->
+val interp_type_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
   constr_expr -> types * manual_implicits
 
+val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+  constr_expr -> constr * manual_implicits
+
 val interp_casted_constr_evars : evar_defs ref -> env -> 
   ?impls:full_implicits_env -> constr_expr -> types -> constr
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fa206e7451..4f26cd1eb5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -101,16 +101,13 @@ let definition_message id =
   if_verbose message ((string_of_id id) ^ " is defined")
 
 let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
-  let sigma = Evd.empty in
   let env = Global.env() in
     match comtypopt with
       None -> 
 	let b = abstract_constr_expr com bl in
-	let ib = intern_constr sigma env b in
-	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
-  	let j = Default.understand_judgment sigma env ib in
+	let b, imps = interp_constr_evars_impls env b in
 	  imps,
-	{ const_entry_body = j.uj_val;
+	{ const_entry_body = b;
 	  const_entry_type = None;
           const_entry_opaque = opacity;
 	  const_entry_boxed = boxed }
@@ -118,9 +115,8 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
 	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
-	let ib = intern_gen false sigma env b in
-	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
-	let (body,typ) = destSubCast (Default.understand_gen (OfType None) sigma env ib) in
+	let b, imps = interp_constr_evars_impls env b in
+	let (body,typ) = destSubCast b in
 	  imps,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
@@ -205,8 +201,8 @@ let set_declare_assumption_hook = (:=) declare_assumption_hook
 let declare_assumption idl is_coe k bl c nl=
   if not (Pfedit.refining ()) then 
     let c = generalize_constr_expr c bl in
-    let sigma = ref Evd.empty_evar_defs and env = Global.env () in
-    let c', imps = interp_type_evars_impls sigma env c in
+    let env = Global.env () in
+    let c', imps = interp_type_evars_impls env c in
       !declare_assumption_hook c';
       List.iter (declare_one_assumption is_coe k c' imps nl) idl
   else
@@ -511,7 +507,7 @@ let interp_cstrs evdref env impls mldata arity ind =
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
+  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in
     (cnames, ctyps'', cimpls)
 
 let interp_mutual paramsl indl notations finite = 
@@ -1045,12 +1041,9 @@ let start_proof_com sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let env = Global.env () in
-  let sigma = Evd.empty in
-  let b = generalize_constr_expr t bl in
-  let ib = intern_type sigma env b in
-  let imps = Implicit_quantifiers.implicits_of_rawterm ib in
-  let j = Default.understand_judgment sigma env ib in
-    start_proof id kind j.uj_val
+  let t = generalize_constr_expr t bl in
+  let it, imps = interp_type_evars_impls env t in
+    start_proof id kind it
       (fun str cst -> 
 	maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
 	hook str cst)