diff options
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index a79c9f978..76cf41c50 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -83,6 +83,13 @@ let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') 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'))) + let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft |