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 +++-
 tactics/class_tactics.ml      | 8 +++++---
 test-suite/bugs/closed/4893.v | 4 ++++
 3 files changed, 12 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/4893.v

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
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6e01a676a2..8d6c085e63 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1500,9 +1500,11 @@ let head_of_constr h c =
   let c = head_of_constr c in
   letin_tac None (Name h) c None Locusops.allHyps
 
-let not_evar c = match kind_of_term c with
-| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
-| _ -> Proofview.tclUNIT ()
+let not_evar c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  match Evarutil.kind_of_term_upto sigma c with
+  | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+  | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
   if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v
new file mode 100644
index 0000000000..9a35bcf954
--- /dev/null
+++ b/test-suite/bugs/closed/4893.v
@@ -0,0 +1,4 @@
+Goal True.
+evar (P: Prop).
+assert (H : P); [|subst P]; [exact I|].
+let T := type of H in not_evar T.
-- 
cgit v1.2.3