diff options
| author | Pierre-Marie Pédrot | 2020-04-30 15:35:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | 04a8c766a51b17997d8a9ffcf6f2d7beffc599ce (patch) | |
| tree | b103f2ed0e8957652f1ae8aa8072849a90b292e5 /proofs | |
| parent | 16b2734e050d4c28d5da1a509cd2387cb8cebe6b (diff) | |
Remove a critical call to V82.tactic in Clenvtac.
Despite being marked as a breaking change by myself, it seems that the
underlying condition had been solved in the meantime.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 767f93787d..197d69a481 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,10 +61,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = clenv_pose_metas_as_evars clenv dep_mvs let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - (* ppedrot: a Goal.enter here breaks things, because the tactic below may - solve goals by side effects, while the compatibility layer keeps those - useless goals. That deserves a FIXME. *) - Proofview.V82.tactic begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then @@ -78,9 +75,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = else clenv.evd in let clenv = { clenv with evd = evd' } in - tclTHEN - (tclEVARS (Evd.clear_metas evd')) - (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) + (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))) end let clenv_pose_dependent_evars ?(with_evars=false) clenv = |