diff options
Diffstat (limited to 'plugins/ssr/ssrelim.mli')
| -rw-r--r-- | plugins/ssr/ssrelim.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 66e202b48..0541a13ed 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -13,7 +13,6 @@ open Ssrmatching_plugin val ssrelim : ?ind:(int * EConstr.types array) option ref -> ?is_case:bool -> - ?ist:Ltac_plugin.Tacinterp.interp_sign -> ((Ssrast.ssrhyps option * Ssrast.ssrocc) * Ssrmatching.cpattern) list -> @@ -28,16 +27,14 @@ val ssrelim : as 'a) -> ?elim:EConstr.constr -> Ssrast.ssripat option -> - (?ist:Ltac_plugin.Tacinterp.interp_sign -> - 'a -> + ( 'a -> Ssrast.ssripat option -> (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) -> bool -> Ssrast.ssrhyp list -> Tacmach.tactic) -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val elimtac : - EConstr.constr -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +val elimtac : EConstr.constr -> unit Proofview.tactic + val casetac : EConstr.constr -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma @@ -48,6 +45,9 @@ val perform_injection : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrscasetac : - bool -> EConstr.constr -> - Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + unit Proofview.tactic + +val ssrscase_or_inj_tac : + EConstr.constr -> + unit Proofview.tactic |