diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /tactics/hiddentac.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'tactics/hiddentac.mli')
-rw-r--r-- | tactics/hiddentac.mli | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 9270411a..36b0830d 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names @@ -37,30 +37,30 @@ val h_exact : constr -> tactic val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic -val h_apply : advanced_flag -> evars_flag -> - open_constr with_bindings list -> tactic -val h_apply_in : advanced_flag -> evars_flag -> - open_constr with_bindings list -> +val h_apply : advanced_flag -> evars_flag -> + constr with_bindings located list -> tactic +val h_apply_in : advanced_flag -> evars_flag -> + constr with_bindings located list -> identifier * intro_pattern_expr located option -> tactic -val h_elim : evars_flag -> constr with_ebindings -> - constr with_ebindings option -> tactic +val h_elim : evars_flag -> constr with_bindings -> + constr with_bindings option -> tactic val h_elim_type : constr -> tactic -val h_case : evars_flag -> constr with_ebindings -> tactic +val h_case : evars_flag -> constr with_bindings -> tactic val h_case_type : constr -> tactic val h_mutual_fix : hidden_flag -> identifier -> int -> (identifier * int * constr) list -> tactic val h_fix : identifier option -> int -> tactic -val h_mutual_cofix : hidden_flag -> identifier -> +val h_mutual_cofix : hidden_flag -> identifier -> (identifier * constr) list -> tactic val h_cofix : identifier option -> tactic -val h_cut : constr -> tactic -val h_generalize : constr list -> tactic -val h_generalize_gen : (constr with_occurrences * name) list -> tactic -val h_generalize_dep : constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> +val h_cut : constr -> tactic +val h_generalize : constr list -> tactic +val h_generalize_gen : (constr with_occurrences * name) list -> tactic +val h_generalize_dep : constr -> tactic +val h_let_tac : letin_flag -> name -> constr -> Tacticals.clause -> tactic (* Derived basic tactics *) @@ -68,20 +68,20 @@ val h_let_tac : letin_flag -> name -> constr -> val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic -val h_new_induction : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> +val h_new_induction : evars_flag -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic -val h_new_destruct : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> +val h_new_destruct : evars_flag -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - (constr with_ebindings induction_arg list * constr with_ebindings option * - (intro_pattern_expr located option * intro_pattern_expr located option) * - Tacticals.clause option) list -> tactic + (constr with_bindings induction_arg list * constr with_bindings option * + (intro_pattern_expr located option * intro_pattern_expr located option)) list + * Tacticals.clause option -> tactic -val h_specialize : int option -> constr with_ebindings -> tactic +val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic (* Automation tactic : see Auto *) @@ -95,10 +95,10 @@ val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic (* Constructors *) -val h_constructor : evars_flag -> int -> open_constr bindings -> tactic -val h_left : evars_flag -> open_constr bindings -> tactic -val h_right : evars_flag -> open_constr bindings -> tactic -val h_split : evars_flag -> open_constr bindings -> tactic +val h_constructor : evars_flag -> int -> constr bindings -> tactic +val h_left : evars_flag -> constr bindings -> tactic +val h_right : evars_flag -> constr bindings -> tactic +val h_split : evars_flag -> constr bindings list -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic @@ -108,15 +108,15 @@ val h_simplest_right : tactic (* Conversion *) val h_reduce : Redexpr.red_expr -> Tacticals.clause -> tactic val h_change : - constr with_occurrences option -> constr -> Tacticals.clause -> tactic + Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic (* Equivalence relations *) val h_reflexivity : tactic val h_symmetry : Tacticals.clause -> tactic -val h_transitivity : constr -> tactic +val h_transitivity : constr option -> tactic -val h_simplest_apply : constr -> tactic -val h_simplest_eapply : constr -> tactic +val h_simplest_apply : constr -> tactic +val h_simplest_eapply : constr -> tactic val h_simplest_elim : constr -> tactic val h_simplest_case : constr -> tactic |