From 62adf2b9e03afa212fcd8819226da068bf4a32b8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 29 Oct 2019 13:20:04 +0100
Subject: 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
---
 pretyping/pretyping.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'pretyping/pretyping.ml')

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
 
-- 
cgit v1.2.3