Pretyping.check_evars: make initial evar map optional

There are no users in Coq but maybe some plugin wants it so don't
completely remove it

8 files changed, 21 insertions, 19 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index ca5c8b30c2..98d14f3d33 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1930,7 +1930,7 @@ let build_morphism_signature env sigma m =
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
-  Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
+  Pretyping.check_evars env evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4925f3e5fa..44b3d59287 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -288,16 +288,18 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 
 (* [check_evars] fails if some unresolved evar remains *)
 
-let check_evars env initial_sigma sigma c =
+let check_evars env ?initial sigma c =
   let rec proc_rec c =
     match EConstr.kind sigma c with
     | Evar (evk, _) ->
-      if not (Evd.mem initial_sigma evk) then
-        let (loc,k) = evar_source evk sigma in
-        begin match k with
-          | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-          | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
-        end
+      (match initial with
+       | Some initial when Evd.mem initial evk -> ()
+       | _ ->
+         let (loc,k) = evar_source evk sigma in
+         begin match k with
+           | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+           | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
+         end)
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index f9da568c75..4aaf1376ad 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -115,9 +115,10 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
 val check_evars_are_solved :
   program_mode:bool -> 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] *)
-val check_evars : env -> evar_map -> evar_map -> constr -> unit
+(** [check_evars env ?initial sigma c] fails if some unresolved evar
+   remains in [c] which isn't in [initial] (any unresolved evar if
+   [initial] not provided) *)
+val check_evars : env -> ?initial:evar_map -> evar_map -> constr -> unit
 
 (**/**)
 (** Internal of Pretyping... *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index eb50a2a67c..7b3797119a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1289,8 +1289,7 @@ let prepare_hint check env init (sigma,c) =
       mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
     let env = Global.env () in
-    let empty_sigma = Evd.from_env env in
-    if check then Pretyping.check_evars env empty_sigma sigma c';
+    if check then Pretyping.check_evars env sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     (c', diff)
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0333b73ffe..c9b5144299 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env =
   (* Beware of this step, it is required as to minimize universes. *)
   let sigma = Evd.minimize_universes sigma in
   (* Check that the type is free of evars now. *)
-  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+  Pretyping.check_evars env sigma termtype;
   termtype, sigma
 
 let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a001420f74..8a403e5a03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -255,7 +255,7 @@ let context ~poly l =
   let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma = Evd.minimize_universes sigma in
-  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
+  let ce t = Pretyping.check_evars env sigma t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
   (* reorder, evar-normalize and add implicit status *)
   let ctx = List.rev_map (fun d ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2aee9bd47f..2afb5e9d65 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -369,10 +369,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
   let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
   let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
-  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
-  Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
+  List.iter (fun c -> check_evars env_params sigma (EConstr.of_constr (snd c))) arities;
+  Context.Rel.iter (fun c -> check_evars env0 sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
-    List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
+    List.iter (fun c -> check_evars env_ar_params sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
diff --git a/vernac/record.ml b/vernac/record.ml
index d85b71df44..5be911938b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
   in
   let univs = Evd.check_univ_decl ~poly sigma decl in
   let ubinders = Evd.universe_binders sigma in
-  let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
+  let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
   let () = List.iter (iter_constr ce) (List.rev newps) in
   ubinders, univs, template, newps, imps, ans