diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 0e4c1eb73..a08468865 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -261,6 +261,10 @@ module New : sig val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic val onClause : (identifier option -> unit tactic) -> clause -> unit tactic + val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family + val elimination_then : (branch_args -> unit Proofview.tactic) -> (arg_bindings * arg_bindings) -> constr -> unit Proofview.tactic |