diff options
| author | aspiwack | 2013-11-02 15:38:32 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:38:32 +0000 |
| commit | 00d30f5330f4f1dd487d5754a0fb855a784efbf0 (patch) | |
| tree | def0f4e640f71192748a2e964b92b9418970a98d /proofs/clenvtac.ml | |
| parent | ea879916e09cd19287c831152d7ae2a84c61f4b0 (diff) | |
Tachmach.New is now in Proofview.Goal.enter style.
As a result the use of the glist-style interface for manipulating goals has almost been removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7874f5ac66..f852995a08 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -85,10 +85,12 @@ let elim_res_pf_THEN_i clenv tac gls = open Proofview.Notations let new_elim_res_pf_THEN_i clenv tac = - Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>= fun clenv' -> - Proofview.tclTHEN - (Proofview.V82.tactic (clenv_refine false clenv')) - (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv'))) + Proofview.Goal.enter begin fun gl -> + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in + Proofview.tclTHEN + (Proofview.V82.tactic (clenv_refine false clenv')) + (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv'))) + end let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft |