Merge pull request #519 from ppedrot/sort-poly-stub

Adapt w.r.t. coq/coq#16903.

src/depelim.ml

@@ -185,6 +185,7 @@ let depcase ~poly ((mind, i as ind), u) =
         :: ((Array.rev_to_list branches)
             @ (make_assum (nameR (Id.of_string "P")) pred :: ctx)))
   in
+  let () = evd := Evd.minimize_universes !evd in
   let univs = Evd.univ_entry ~poly !evd in
   let ce = Declare.definition_entry ~univs (EConstr.to_constr !evd body) in
   let kn =

src/equations_common.ml

@@ -1079,7 +1079,7 @@ let nonalgebraic_universe_level_of_universe env sigma u =
   match ESorts.kind sigma u with
   | Sorts.Set | Sorts.Prop | Sorts.SProp ->
     sigma, Univ.Level.set, u
-  | Sorts.Type u0 ->
+  | Sorts.Type u0 | Sorts.QSort (_, u0) ->
     match Univ.Universe.level u0 with
     | Some l ->
       (match Evd.universe_rigidity sigma l with

src/noconf.ml

@@ -93,7 +93,7 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
     | Sorts.InSProp -> mkSProp
     | Sorts.InProp -> mkProp
     | Sorts.InSet -> mkSet
-    | Sorts.InType ->
+    | Sorts.InType | Sorts.InQSort ->
       (* In that case the noConfusion principle lives at the level of the type. *)
       let sort = EConstr.mkSort (ESorts.make inds) in
       let sigma, s =

src/noconf_hom.ml

@@ -132,11 +132,11 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
   let fullbinders = ydecl :: binders in
   let sigma, s =
     match Lazy.force logic_sort with
-    | Sorts.InType | Sorts.InSet -> (* In that case noConfusion lives at the level of the inductive family *)
+    | Sorts.InType | Sorts.InSet | Sorts.InQSort -> (* In that case noConfusion lives at the level of the inductive family *)
       let sort = EConstr.mkSort (ESorts.make inds) in
       let is_level = match inds with
       | Sorts.Prop | Sorts.SProp | Sorts.Set -> true
-      | Sorts.Type u -> Univ.Universe.is_level u
+      | Sorts.Type u | Sorts.QSort (_, u) -> Univ.Universe.is_level u
       in
       if is_level then sigma, sort
       else

src/principles.ml

@@ -1424,6 +1424,7 @@ let max_sort s1 s2 =
   | (Prop, (Set | Type _ as s)) | ((Set | Type _) as s, Prop) -> s
   | (Set, Type u) | (Type u, Set) -> Sorts.sort_of_univ (Univ.Universe.sup Univ.Universe.type0 u)
   | (Type u, Type v) -> Sorts.sort_of_univ (Univ.Universe.sup u v)
+  | (QSort _, _) | (_, QSort _) -> assert false
 
 let level_of_context env evd ctx acc =
   let _, lev =

src/subterm.ml

@@ -46,7 +46,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) =
     | Sorts.InSProp -> failwith "not implemented"
     | Sorts.InProp -> mkProp
     | Sorts.InSet -> mkSet
-    | Sorts.InType -> EConstr.mkSort (ESorts.make indsort)
+    | Sorts.InType | Sorts.InQSort -> EConstr.mkSort (ESorts.make indsort)
   in
   let len = List.length ctx in
   let params = mind.mind_nparams_rec in