diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index b4491770e..f81698370 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -25,9 +25,9 @@ open Misctypes (** Basic tactics *) -val h_intro_move : Id.t option -> Id.t move_location -> tactic -val h_intro : Id.t -> tactic -val h_intros_until : quantified_hypothesis -> tactic +val h_intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic +val h_intro : Id.t -> unit Proofview.tactic +val h_intros_until : quantified_hypothesis -> unit Proofview.tactic val h_assumption : tactic val h_exact : constr -> tactic @@ -38,12 +38,12 @@ 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 -> - Id.t * intro_pattern_expr located option -> tactic + Id.t * intro_pattern_expr located option -> unit Proofview.tactic val h_elim : evars_flag -> constr with_bindings -> - constr with_bindings option -> tactic + constr with_bindings option -> unit Proofview.tactic val h_elim_type : constr -> tactic -val h_case : evars_flag -> constr with_bindings -> tactic +val h_case : evars_flag -> constr with_bindings -> unit Proofview.tactic val h_case_type : constr -> tactic val h_mutual_fix : Id.t -> int -> @@ -57,31 +57,31 @@ val h_generalize : constr list -> tactic val h_generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic val h_generalize_dep : ?with_let:bool -> constr -> tactic val h_let_tac : letin_flag -> Name.t -> constr -> Locus.clause -> - intro_pattern_expr located option -> tactic + intro_pattern_expr located option -> unit Proofview.tactic val h_let_pat_tac : letin_flag -> Name.t -> evar_map * constr -> Locus.clause -> intro_pattern_expr located option -> - tactic + unit Proofview.tactic (** Derived basic tactics *) -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_simple_induction : quantified_hypothesis -> unit Proofview.tactic +val h_simple_destruct : quantified_hypothesis -> unit Proofview.tactic +val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> unit Proofview.tactic val h_new_induction : evars_flag -> (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> constr with_bindings option -> - Locus.clause option -> tactic + Locus.clause option -> unit Proofview.tactic val h_new_destruct : evars_flag -> (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> constr with_bindings option -> - Locus.clause option -> tactic + Locus.clause option -> unit Proofview.tactic val h_induction_destruct : rec_flag -> evars_flag -> ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list * constr with_bindings option - * Locus.clause option -> tactic + * Locus.clause option -> unit Proofview.tactic val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic @@ -97,14 +97,14 @@ val h_rename : (Id.t*Id.t) list -> tactic val h_revert : Id.t list -> tactic (** Constructors *) -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_constructor : evars_flag -> int -> constr bindings -> unit Proofview.tactic +val h_left : evars_flag -> constr bindings -> unit Proofview.tactic +val h_right : evars_flag -> constr bindings -> unit Proofview.tactic +val h_split : evars_flag -> constr bindings list -> unit Proofview.tactic -val h_one_constructor : int -> tactic -val h_simplest_left : tactic -val h_simplest_right : tactic +val h_one_constructor : int -> unit Proofview.tactic +val h_simplest_left : unit Proofview.tactic +val h_simplest_right : unit Proofview.tactic (** Conversion *) @@ -113,13 +113,13 @@ val h_change : Pattern.constr_pattern option -> constr -> Locus.clause -> tactic (** Equivalence relations *) -val h_reflexivity : tactic -val h_symmetry : Locus.clause -> tactic -val h_transitivity : constr option -> tactic +val h_reflexivity : unit Proofview.tactic +val h_symmetry : Locus.clause -> unit Proofview.tactic +val h_transitivity : constr option -> unit Proofview.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 +val h_simplest_elim : constr -> unit Proofview.tactic +val h_simplest_case : constr -> unit Proofview.tactic -val h_intro_patterns : intro_pattern_expr located list -> tactic +val h_intro_patterns : intro_pattern_expr located list -> unit Proofview.tactic |