Merge PR #8933: Make initial evar map argument to check_evars_are_solved optional.

6 files changed, 6 insertions, 7 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index ef28fc2d77..4cdc60216e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -156,7 +156,7 @@ let do_assumptions kind nl l =
       ((sigma,env,ienv),((is_coe,idl),t,imps)))
     (sigma,env,empty_internalization_env) l
   in
-  let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in
+  let sigma = solve_remaining_evars all_and_fail_flags env sigma in
   (* The universe constraints come from the whole telescope. *)
   let sigma = Evd.minimize_universes sigma in
   let nf_evar c = EConstr.to_constr sigma c in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 472411ac3a..9c80f1d2f5 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -87,8 +87,7 @@ let interp_definition pl bl poly red_option c ctypopt =
 
 let check_definition (ce, evd, _, imps) =
   let env = Global.env () in
-  let empty_sigma = Evd.from_env env in
-  check_evars_are_solved env evd empty_sigma;
+  check_evars_are_solved env evd;
   ce
 
 let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a9c499b192..274c99107f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -239,7 +239,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
   end
 
 let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
-  check_evars_are_solved env evd (Evd.from_env env);
+  check_evars_are_solved env evd;
   let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
   Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f405c4d5a9..fbfa997555 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -402,7 +402,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
+  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index de020926f6..2443c5d12a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -421,7 +421,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
     let flags = all_and_fail_flags in
     let hook = inference_hook in
-    let evd = solve_remaining_evars ?hook flags env evd Evd.empty in
+    let evd = solve_remaining_evars ?hook flags env evd in
     let ids = List.map RelDecl.get_name ctx in
     check_name_freshness (pi1 kind) id;
     (* XXX: The nf_evar is critical !! *)
diff --git a/vernac/record.ml b/vernac/record.ml
index ac84003266..7bdf6a973f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -160,7 +160,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
   in
   let (sigma, data) = List.fold_left2_map fold sigma records arities in
   let sigma =
-    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in
+    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
   let fold sigma (typ, sort) (_, newfs) =
     let _, univ = compute_constructor_level sigma env_ar newfs in
       if not def && (Sorts.is_prop sort ||