From 41840f92c0ee8c10691411f2a44e4059a4754456 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 4 Nov 2020 13:16:55 +0100
Subject: Small cleanup in ComInductive

---
 vernac/comInductive.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index bb26ce652e..cc3f7bc093 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -271,9 +271,8 @@ let inductive_levels env evd arities inds =
     if Sorts.is_prop a || Sorts.is_sprop a then None
     else Some (univ_of_sort a)) destarities
   in
-  let cstrs_levels, min_levels, sizes =
-    CList.split3
-      (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
+  let cstrs_levels, sizes =
+    CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
@@ -283,13 +282,15 @@ let inductive_levels env evd arities inds =
         in
         let minlev =
           (* Indices contribute. *)
-          if indices_matter env && List.length ctx > 0 then (
+          if indices_matter env then begin
             let ilev = sign_level env evd ctx in
-              Univ.sup ilev minlev)
+            Univ.sup ilev minlev
+          end
           else minlev
         in
         let clev = extract_level env evd minlev tys in
-          (clev, minlev, len)) inds destarities)
+        (clev, len))
+        inds destarities)
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
-- 
cgit v1.2.3


From f09eef2a1c55a1e9a617b7bad0759b4760a8978a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 4 Nov 2020 15:02:11 +0100
Subject: Only lower inductives to Prop if the type is syntactically an arity.

Fix #13300
---
 test-suite/bugs/closed/bug_13300.v | 7 +++++++
 vernac/comInductive.ml             | 9 +++++++--
 2 files changed, 14 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13300.v

diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v
new file mode 100644
index 0000000000..e4fcd6dacc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13300.v
@@ -0,0 +1,7 @@
+Polymorphic Definition type := Type.
+
+Inductive bad : type := .
+
+Fail Check bad : Prop.
+Check bad : Set.
+(* lowered as much as possible *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc3f7bc093..6cf6606a93 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -327,8 +327,13 @@ let inductive_levels env evd arities inds =
         let duu = Sorts.univ_of_sort du in
         let template_prop, evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
-            if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              true, Evd.set_eq_sort env evd Sorts.prop du
+            if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu)
+            then if Term.isArity arity
+            (* If not a syntactic arity, the universe may be used in a
+               polymorphic instance and so cannot be lowered to Prop.
+               See #13300. *)
+              then true, Evd.set_eq_sort env evd Sorts.prop du
+              else false, Evd.set_eq_sort env evd Sorts.set du
             else false, evd
           else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
         in
-- 
cgit v1.2.3