diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-24 14:23:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-24 15:52:31 +0200 |
| commit | 03cab057c3ccc51464ed69531441d3c09b2919a7 (patch) | |
| tree | af11609b17ae021e10ffad2edf2386fcdb0dc70f /tactics/class_tactics.ml | |
| parent | 89dc208ff140ba6ecd7b2c931401f9c58fb2985e (diff) | |
Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it
exhibits the "useless goal" behaviour: there is code out there depending on
the fact that goals cannot be solved by side effects.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f11c027ad..7c9aa59b6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -104,13 +104,13 @@ let unify_e_resolve poly flags (c,clenv) gls = let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in let clenv' = connect_clenv gls clenv' in let clenv' = clenv_unique_resolver ~flags clenv' gls in - Clenvtac.clenv_refine true ~with_classes:false clenv' gls + Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls let unify_resolve poly flags (c,clenv) gls = let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in let clenv' = connect_clenv gls clenv' in let clenv' = clenv_unique_resolver ~flags clenv' gls in - Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv' gls + Proofview.V82.of_tactic (Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv') gls let clenv_of_prods poly nprods (c, clenv) gls = if poly || Int.equal nprods 0 then Some clenv |