aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hiddentac.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hiddentac.mli')
-rw-r--r--tactics/hiddentac.mli54
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