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

10 files changed, 22 insertions, 17 deletions

diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh
new file mode 100644
index 0000000000..e74e53fa40
--- /dev/null
+++ b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then
+    plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg
+    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
+fi
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8c57fc2375..abf52d2893 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -215,7 +215,7 @@ type frozen =
   (** Proper partition of the evar map as described above. *)
 
 let frozen_and_pending_holes (sigma, sigma') =
-  let undefined0 = Evd.undefined_map sigma in
+  let undefined0 = Option.cata Evd.undefined_map Evar.Map.empty sigma in
   (** Fast path when the undefined evars where not modified *)
   if undefined0 == Evd.undefined_map sigma' then
     FrozenId undefined0
@@ -306,8 +306,8 @@ let check_evars_are_solved env sigma frozen =
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
-let solve_remaining_evars ?hook flags env sigma init_sigma =
-  let frozen = frozen_and_pending_holes (init_sigma, sigma) in
+let solve_remaining_evars ?hook flags env ?initial sigma =
+  let frozen = frozen_and_pending_holes (initial, sigma) in
   let sigma =
     if flags.use_typeclasses
     then apply_typeclasses env sigma frozen false
@@ -324,12 +324,12 @@ let solve_remaining_evars ?hook flags env sigma init_sigma =
   if flags.fail_evar then check_evars_are_solved env sigma frozen;
   sigma
 
-let check_evars_are_solved env current_sigma init_sigma =
-  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
+let check_evars_are_solved env ?initial current_sigma =
+  let frozen = frozen_and_pending_holes (initial, current_sigma) in
   check_evars_are_solved env current_sigma frozen
 
-let process_inference_flags flags env initial_sigma (sigma,c,cty) =
-  let sigma = solve_remaining_evars flags env sigma initial_sigma in
+let process_inference_flags flags env initial (sigma,c,cty) =
+  let sigma = solve_remaining_evars flags env ~initial sigma in
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c,cty
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2eaa77b822..59e6c00037 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -95,13 +95,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
    [pending], however, it can contain more evars than the pending ones. *)
 
 val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
-  env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
+  env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map
 
 (** Checking evars and pending conversion problems are all solved,
     reporting an appropriate error message *)
 
 val check_evars_are_solved :
-  env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit
+  env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 490d58fa52..8c1aae26ae 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1530,7 +1530,7 @@ let indirectly_dependent sigma c d decls =
     List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
-  let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
+  let sigma = Pretyping.solve_remaining_evars flags env current_sigma ~initial:pending in
   (sigma, nf_evar sigma c)
 
 let default_matching_core_flags sigma =
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 ||