diff options
| author | Gaëtan Gilbert | 2020-02-12 12:56:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 12:56:22 +0100 |
| commit | 0709808440c67832d170c32ff9ee6ac993061144 (patch) | |
| tree | 728a4336c9a2d94e645f27c438e2908fcc5bc289 /vernac/comInductive.mli | |
| parent | 2a4d9569570584c300fcb19c3804fe07578eef12 (diff) | |
| parent | b6264bb2df9b73b905af126ede49cd31abf0e7da (diff) | |
Merge PR #11546: Remove the Template Check option.
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
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. *) |