From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 18:47:45 +0200
Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

---
 ltac/extratactics.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index be47293fcd..e50b0520bc 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -816,9 +816,11 @@ END
 
 TACTIC EXTEND is_evar
 | [ "is_evar" constr(x) ] ->
-    [ match kind_of_term x with
+    [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
+      match Evarutil.kind_of_term_upto sigma x with
         | Evar _ -> Proofview.tclUNIT ()
         | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
+      end
     ]
 END
 
-- 
cgit v1.2.3