aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/elim.mli')
-rw-r--r--tactics/elim.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli
index b0fb3981f..0fb104310 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -22,7 +22,8 @@ val introElimAssumsThen :
(branch_assumptions -> tactic) -> branch_args -> tactic
val introCaseAssumsThen :
- (branch_assumptions -> tactic) -> branch_args -> tactic
+ (Tacexpr.intro_pattern_expr list -> branch_assumptions -> tactic) ->
+ branch_args -> tactic
val general_decompose : (identifier * constr -> bool) -> constr -> tactic
val decompose_nonrec : constr -> tactic