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