Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

3 files changed, 12 insertions, 4 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index be47293fc..e50b0520b 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 6e01a676a..8d6c085e6 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 000000000..9a35bcf95
--- /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.