diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 56d6f7f09a..5ad21c2a5b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -158,17 +158,17 @@ let e_give_exact flags h = in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> - Clenvtac.unify ~flags t1 <*> exact_no_check c + Clenv.unify ~flags t1 <*> exact_no_check c end let unify_e_resolve flags = begin fun gls (h, _) -> let clenv', c = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:true ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' end let unify_resolve flags = begin fun gls (h, _) -> let clenv', _ = connect_hint_clenv h gls in - Clenvtac.res_pf ~with_evars:false ~with_classes:false ~flags clenv' + Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' end (** Application of a lemma using [refine] instead of the old [w_unify] *) |