diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index f84c95c6aa..8285b81670 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -66,6 +66,8 @@ val constructor_nrealhyps : env -> constructor -> int val get_full_arity_sign : env -> inductive -> rel_context +val allowed_sorts : env -> inductive -> sorts_family list + (* Extract information from an inductive family *) type constructor_summary = { |