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
---
 vernac/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

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