diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index cc104b3762..1286e4a5c3 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : template_check:bool - -> ctor_levels:Univ.LSet.t + : ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params +(** [template_polymorphism_candidate ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] 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. *) + conclusion sort, if one is given. *) |