From a5d124dd7c3d43a5ead81cfac30c7d1448002d56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Nov 2019 15:53:48 +0100
Subject: Fix #11039: proof of False with template poly and nonlinear universes

Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.
---
 kernel/indTyping.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8da4e2885c..5c04e860a2 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -38,6 +38,7 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
    of a template polymorphic inductive *)
 val template_polymorphic_univs :
   template_check:bool ->
+  ctor_levels:Univ.LSet.t ->
   Univ.ContextSet.t ->
   Constr.rel_context ->
   Univ.Universe.t ->
-- 
cgit v1.2.3