diff options
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 76cf41c507..7874f5ac66 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -85,7 +85,7 @@ 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' -> + 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'))) |