aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/inv.mli')
-rw-r--r--tactics/inv.mli22
1 files changed, 11 insertions, 11 deletions
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 52db199ee..9491b7d7b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -19,24 +19,24 @@ type inversion_status = Dep of constr option | NoDep
val inv_gen :
bool -> inversion_kind -> inversion_status ->
- intro_pattern_expr located option -> quantified_hypothesis -> tactic
+ intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
val invIn_gen :
inversion_kind -> intro_pattern_expr located option -> Id.t list ->
- quantified_hypothesis -> tactic
+ quantified_hypothesis -> unit Proofview.tactic
val inv_clause :
inversion_kind -> intro_pattern_expr located option -> Id.t list ->
- quantified_hypothesis -> tactic
+ quantified_hypothesis -> unit Proofview.tactic
val inv : inversion_kind -> intro_pattern_expr located option ->
- quantified_hypothesis -> tactic
+ quantified_hypothesis -> unit Proofview.tactic
val dinv : inversion_kind -> constr option ->
- intro_pattern_expr located option -> quantified_hypothesis -> tactic
+ intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic
-val half_inv_tac : Id.t -> tactic
-val inv_tac : Id.t -> tactic
-val inv_clear_tac : Id.t -> tactic
-val half_dinv_tac : Id.t -> tactic
-val dinv_tac : Id.t -> tactic
-val dinv_clear_tac : Id.t -> tactic
+val half_inv_tac : Id.t -> unit Proofview.tactic
+val inv_tac : Id.t -> unit Proofview.tactic
+val inv_clear_tac : Id.t -> unit Proofview.tactic
+val half_dinv_tac : Id.t -> unit Proofview.tactic
+val dinv_tac : Id.t -> unit Proofview.tactic
+val dinv_clear_tac : Id.t -> unit Proofview.tactic