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

3 files changed, 10 insertions, 10 deletions

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 =