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
---
 tactics/hints.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics')

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