diff options
| author | Pierre-Marie Pédrot | 2016-08-30 18:47:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-30 19:03:05 +0200 |
| commit | 4582ed1c8f0620941a3c296941b1dc808c95d7fe (patch) | |
| tree | d9d58f831b051fa06c5d014f663299db8f91ae35 /ltac | |
| parent | 721637c98514a77d05d080f53f226cab3a8da1e7 (diff) | |
Fix bug #4893: not_evar: unexpected failure in 8.5pl1.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 4 |
1 files changed, 3 insertions, 1 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 |