Interp a definition with the implicit arguments of its local context

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

4 files changed, 16 insertions, 16 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9b6c74398a..3084da768a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -136,8 +136,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
-    let (env', ctx), imps = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in
+    let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
+    let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
@@ -276,7 +276,7 @@ let named_of_rel_context l =
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref Evd.empty in
-  let (env', fullctx), impls = interp_context_evars evars env l in
+  let _, ((env', fullctx), impls) = interp_context_evars evars env l in
   let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c180785d56..ae173f6c39 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -67,11 +67,11 @@ let red_constant_entry n ce = function
 let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
+  let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
   let imps,ce =
     match ctypopt with
       None ->
-	let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in
+	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	check_evars env Evd.empty !evdref body;
 	imps1@imps2,
@@ -79,8 +79,8 @@ let interp_definition bl red_option c ctypopt =
 	  const_entry_type = None;
           const_entry_opaque = false }
     | Some ctyp ->
-	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
-	let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
+	let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
+	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
 	check_evars env Evd.empty !evdref body;
@@ -221,7 +221,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref Evd.empty in
-  let (env_params, ctx_params), userimpls =
+  let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars evdref env0 paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
@@ -451,8 +451,8 @@ type structured_fixpoint_expr = {
 
 let interp_fix_context evdref env isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
-  let (env', ctx), imps = interp_context_evars evdref env before in
-  let (env'', ctx'), imps' = interp_context_evars evdref env' after in
+  let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in
+  let _, ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), imps @ imps', annot)
       
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index c0ce16ceae..2d904c5546 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -313,8 +313,8 @@ let start_proof_com kind thms hook =
   let evdref = ref (create_evar_defs Evd.empty) in
   let env0 = Global.env () in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
-    let (env, ctx), imps = interp_context_evars evdref env0 bl in
-    let t', imps' = interp_type_evars_impls ~evdref env t in
+    let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
+    let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
     Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
     let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 74a33f6f9e..0255e6504d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -33,7 +33,7 @@ let interp_evars evdref env impls k typ =
   let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
-let interp_fields_evars evars env nots l =
+let interp_fields_evars evars env impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
       let impl, t' = interp_evars evars env impls Pretyping.IsType t in
@@ -46,7 +46,7 @@ let interp_fields_evars evars env nots l =
       let d = (i,b',t') in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], empty_internalization_env) nots l
+    (env, [], [], impls_env) nots l
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -69,11 +69,11 @@ let typecheck_params_and_fields id t ps nots fs =
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
   in 
-  let (env1,newps), imps = interp_context_evars evars env0 ps in
+  let impls_env, ((env1,newps), imps) = interp_context_evars evars env0 ps in
   let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,impls,newfs,data =
-    interp_fields_evars evars env_ar nots (binders_of_decls fs)
+    interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
   in
   let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
   let evars = Typeclasses.resolve_typeclasses env_ar evars in