diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index a77cd66a33..2d4cd7cac2 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -77,3 +77,11 @@ val interp_mutual_inductive : decl_notation list -> cumulative_inductive_flag -> poly:bool -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list |