Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear universes

Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot

1 files changed, 15 insertions, 9 deletions

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 45e539b1e4..ef05b213d8 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -77,12 +77,18 @@ val should_auto_template : Id.t -> bool -> bool
    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 template_polymorphism_candidate
+  : Environ.env
+  -> ctor_levels:Univ.LSet.t
+  -> Entries.universes_entry
+  -> Constr.rel_context
+  -> Sorts.t option
+  -> bool
+(** [template_polymorphism_candidate env ~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. *)