diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 46 |
1 files changed, 33 insertions, 13 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b7ab31c4..d39433d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 11166 2008-06-22 13:23:35Z herbelin $ i*) +(*i $Id: tactics.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) +open Util open Names open Term open Environ @@ -68,7 +69,8 @@ val find_intro_names : rel_context -> goal sigma -> identifier list val intro : tactic val introf : tactic val intro_force : bool -> tactic -val intro_move : identifier option -> identifier option -> tactic +val intro_move : identifier option -> identifier move_location -> tactic + (* [intro_avoiding idl] acts as intro but prevents the new identifier to belong to [idl] *) val intro_avoiding : identifier list -> tactic @@ -110,9 +112,10 @@ val onInductionArg : (*s Introduction tactics with eliminations. *) -val intro_pattern : identifier option -> intro_pattern_expr -> tactic -val intro_patterns : intro_pattern_expr list -> tactic -val intros_pattern : identifier option -> intro_pattern_expr list -> tactic +val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic +val intro_patterns : intro_pattern_expr located list -> tactic +val intros_pattern : + identifier move_location -> intro_pattern_expr located list -> tactic (*s Exact tactics. *) @@ -167,7 +170,7 @@ val keep : identifier list -> tactic val specialize : int option -> constr with_ebindings -> tactic -val move_hyp : bool -> identifier -> identifier -> tactic +val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier * identifier) list -> tactic val revert : identifier list -> tactic @@ -183,7 +186,7 @@ val apply_without_reduce : constr -> tactic val apply_list : constr list -> tactic val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> constr with_ebindings -> tactic + advanced_flag -> evars_flag -> constr with_ebindings list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic @@ -260,7 +263,9 @@ val elim : val simple_induct : quantified_hypothesis -> tactic val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic + constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Case analysis tactics. *) @@ -269,7 +274,18 @@ val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic + constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic + +(*s Generic case analysis / induction tactics. *) + +val induction_destruct : evars_flag -> rec_flag -> + (constr with_ebindings induction_arg list * + constr with_ebindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + clause option) list -> + tactic (*s Eliminations giving the type instead of the proof. *) @@ -330,20 +346,24 @@ val cut_replacing : identifier -> constr -> (tactic -> tactic) -> tactic val cut_in_parallel : constr list -> tactic -val assert_as : bool -> intro_pattern_expr -> constr -> tactic -val forward : tactic option -> intro_pattern_expr -> constr -> tactic -val letin_tac : bool option -> name -> constr -> clause -> tactic +val assert_as : bool -> intro_pattern_expr located -> constr -> tactic +val forward : tactic option -> intro_pattern_expr located -> constr -> tactic +val letin_tac : (bool * intro_pattern_expr located) option -> name -> + constr -> clause -> tactic val true_cut : name -> constr -> tactic val assert_tac : bool -> name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic val generalize_dep : constr -> tactic +val conv : constr -> constr -> tactic +val resolve_classes : tactic + val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic -val abstract_generalize : identifier -> tactic +val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit |