diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 00ce4da8d5..6cd63fa6ad 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -146,6 +146,7 @@ val compute_induction_names : val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family +val elimination_sort_of_clause : identifier option -> goal sigma -> sorts_family val general_elim_then_using : (inductive -> goal sigma -> constr) -> rec_flag -> |