diff options
| author | Pierre-Marie Pédrot | 2014-06-23 17:22:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-23 17:23:09 +0200 |
| commit | c92bb5b1da8223d61e0ac63a4ebd4a54f46d4670 (patch) | |
| tree | 22cfaa670d79703746145b95b2b59b1b36810a92 /tactics | |
| parent | 1f7665f8cac6002ff1c76db5cc6e2a5c8f261ee7 (diff) | |
Clenvtac.unify is in the new monad.
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) |