diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 31fbc0661d..f11c027ad4 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -98,7 +98,7 @@ let e_give_exact flags poly (c,clenv) gl = else c, gl in let t1 = pf_type_of gl c in - tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl + tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index bc3ad026cb..98e7d3ff5f 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -34,7 +34,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then - tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl + tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl else Proofview.V82.of_tactic (exact_check c) gl let assumption id = e_give_exact (mkVar id) |