diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 285be8cd51..7587bd165f 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) + +val template_polymorphism_candidate : + Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool +(** [template_polymorphism_candidate env uctx params conclsort] is + [true] iff an inductive with params [params] and conclusion + [conclsort] would be definable as template polymorphic. It should + have at least one universe in its monomorphic universe context that + can be made parametric in its conclusion sort, if one is given. + If the [Template Check] flag is false we just check that the conclusion sort + is not small. *) + +val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t +(** [sign_level env sigma ctx] computes the universe level of the context [ctx] + as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) |