diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e97abe9f..6826977b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli 10785 2008-04-13 21:41:54Z herbelin $ i*) +(*i $Id: tacticals.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Pp +open Util open Names open Term open Sign @@ -124,23 +125,30 @@ type branch_args = { nassums : int; (* the number of assumptions to be introduced *) branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) - branchnames : intro_pattern_expr list} + branchnames : intro_pattern_expr located list} type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) +(* [check_disjunctive_pattern_size loc pats n] returns an appropriate *) +(* error message if |pats| <> n *) +val check_or_and_pattern_size : + Util.loc -> or_and_intro_pattern_expr -> int -> unit + (* Useful for [as intro_pattern] modifier *) val compute_induction_names : - int -> intro_pattern_expr -> intro_pattern_expr list array + int -> intro_pattern_expr located option -> + intro_pattern_expr located list array val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family val general_elim_then_using : - (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr -> - (branch_args -> tactic) -> constr option -> - (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic + (inductive -> goal sigma -> constr) -> rec_flag -> + intro_pattern_expr located option -> (branch_args -> tactic) -> + constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> + tactic val elimination_then_using : (branch_args -> tactic) -> constr option -> @@ -151,12 +159,12 @@ val elimination_then : (arg_bindings * arg_bindings) -> constr -> tactic val case_then_using : - intro_pattern_expr -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val case_nodep_then_using : - intro_pattern_expr -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic |