diff options
| -rw-r--r-- | ltac/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4893.v | 4 |
3 files changed, 12 insertions, 4 deletions
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. |