diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index aa4a602525d8a..466675027dec7 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -99,7 +99,25 @@ let check_template ar1 ar2 = match ar1, ar2 with
 | None, Some _ | Some _, None -> false
 
 (* if the generated inductive is squashed the original one must be squashed *)
-let check_squashed k1 k2 = if k2 then k1 else true
+let check_squashed orig generated = match orig, generated with
+  | None, None -> true
+  | Some _, None ->
+    (* the inductive is from functor instantiation which removed the need for squash *)
+    true
+  | None, Some _ ->
+    (* missing squash *)
+    false
+  | Some s1, Some s2 ->
+    (* functor instantiation can change sort qualities
+       (from Type -> Prop)
+       Condition: every quality which can make the generated inductive
+       squashed must also make the original inductive squashed *)
+    match s1, s2 with
+    | AlwaysSquashed, AlwaysSquashed -> true
+    | AlwaysSquashed, SometimesSquashed _ -> true
+    | SometimesSquashed _, AlwaysSquashed -> false
+    | SometimesSquashed s1, SometimesSquashed s2 ->
+      List.for_all (fun s2 -> List.exists (fun s1 -> Sorts.Quality.equal s1 s2) s1) s2
 
 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost
    the knowledge of who is the canonical version.
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e41348530fdf8..72d0ee47a500d 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -164,6 +164,15 @@ type regular_inductive_arity = {
 
 type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
 
+type squash_info =
+  | AlwaysSquashed
+  | SometimesSquashed of Sorts.Quality.t list
+  (** A sort polymorphic inductive [I@{...|...|...} : ... -> Type@{ s|...}]
+      is squashed at a given instantiation if the qualities in the list are not smaller than [s].
+
+      NB: if [s] is sort poly and the inductive has >0 constructors
+      SometimesSquashed contains Prop ie the SProp instantiation is squashed. *)
+
 (** {7 Datas specific to a single type of a block of mutually inductive type } *)
 type one_inductive_body = {
 (** {8 Primitive datas } *)
@@ -198,7 +207,7 @@ type one_inductive_body = {
 
     mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
-    mind_squashed : bool; (** Is elimination restricted to the inductive's sort? *)
+    mind_squashed : squash_info option; (** Is elimination restricted to the inductive's sort? *)
 
     mind_nf_lc : (rel_context * types) array;
  (** Head normalized constructor types so that their conclusion
diff --git a/kernel/genlambda.ml b/kernel/genlambda.ml
index 22723ad67f44b..ac8402e15ce37 100644
--- a/kernel/genlambda.ml
+++ b/kernel/genlambda.ml
@@ -69,11 +69,11 @@ let pp_rel name n =
   Name.print name ++  str "##" ++ int n
 
 let pp_sort s =
-  match Sorts.family s with
-  | Sorts.InSet -> str "Set"
-  | Sorts.InProp -> str "Prop"
-  | Sorts.InSProp -> str "SProp"
-  | Sorts.InType | Sorts.InQSort -> str "Type"
+  match s with
+  | Sorts.Set -> str "Set"
+  | Sorts.Prop -> str "Prop"
+  | Sorts.SProp -> str "SProp"
+  | Sorts.Type _ | Sorts.QSort _ -> str "Type"
 
 let pr_con sp = str(Names.Label.to_string (Constant.label sp))
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 946abd6255892..d39735b7decb4 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -74,7 +74,7 @@ type record_arg_info =
   | HasRelevantArg
 
 type univ_info =
-  { ind_squashed : bool
+  { ind_squashed : squash_info option
   ; record_arg_info : record_arg_info
   ; ind_template : bool
   ; ind_univ : Sorts.t
@@ -94,22 +94,21 @@ let check_univ_leq ?(is_real_arg=false) env u info =
       | Sorts.SProp | QSort _ -> info
       | Prop | Set | Type _ -> { info with record_arg_info = HasRelevantArg }
   in
-  (* If we would squash (eg Prop, SProp case) we still need to check the type in type flag. *)
-  let ind_squashed = not (Environ.type_in_type env) in
-  match u, info.ind_univ with
+  if (Environ.type_in_type env) then info
+  else match u, info.ind_univ with
   | SProp, (SProp | Prop | Set | QSort _ | Type _) ->
     (* Inductive types provide explicit lifting from SProp to other universes,
        so allow SProp <= any. *)
     info
 
-  | Prop, SProp -> { info with ind_squashed }
-  | Prop, QSort _ -> { info with ind_squashed } (* imprecise *)
+  | Prop, SProp -> { info with ind_squashed = Some AlwaysSquashed }
+  | Prop, QSort _ -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
   | Prop, (Prop | Set | Type _) -> info
 
-  | Set, (SProp | Prop) -> { info with ind_squashed }
+  | Set, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed }
   | Set, QSort (_, indu) ->
     if UGraph.check_leq (universes env) Universe.type0 indu
-    then { info with ind_squashed } (* imprecise *)
+    then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
     else { info with missing = u :: info.missing }
   | Set, Set -> info
   | Set, Type indu ->
@@ -117,34 +116,34 @@ let check_univ_leq ?(is_real_arg=false) env u info =
     then info
     else { info with missing = u :: info.missing }
 
-  | QSort _, (SProp | Prop) -> { info with ind_squashed } (* imprecise *)
+  | QSort _, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
   | QSort (cq, uu), QSort (indq, indu) ->
     if UGraph.check_leq (universes env) uu indu
     then begin if Sorts.QVar.equal cq indq then info
-      else { info with ind_squashed } (* imprecise *)
+      else { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
     end
     else { info with missing = u :: info.missing }
   | QSort (_, uu), Set ->
     if UGraph.check_leq (universes env) uu Universe.type0
     then info
     else if is_impredicative_set env
-    then { info with ind_squashed } (* imprecise *)
+    then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
     else { info with missing = u :: info.missing }
   | QSort (_,uu), Type indu ->
     if UGraph.check_leq (universes env) uu indu
     then info
     else { info with missing = u :: info.missing }
 
-  | Type _, (SProp | Prop) -> { info with ind_squashed }
+  | Type _, (SProp | Prop) -> { info with ind_squashed = Some AlwaysSquashed }
   | Type uu, Set ->
     if UGraph.check_leq (universes env) uu Universe.type0
     then info
     else if is_impredicative_set env
-    then { info with ind_squashed }
+    then { info with ind_squashed = Some AlwaysSquashed }
     else { info with missing = u :: info.missing }
   | Type uu, QSort (_, indu) ->
     if UGraph.check_leq (universes env) uu indu
-    then { info with ind_squashed } (* imprecise *)
+    then { info with ind_squashed = Some AlwaysSquashed } (* imprecise *)
     else { info with missing = u :: info.missing }
   | Type uu, Type indu ->
     if UGraph.check_leq (universes env) uu indu
@@ -173,7 +172,7 @@ let check_arity ~template env_params env_ar ind =
   let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
   let indices, ind_sort = Reduction.dest_arity env_params arity in
   let univ_info = {
-    ind_squashed=false;
+    ind_squashed=None;
     record_arg_info=NoRelevantArg;
     ind_template = template;
     ind_univ=ind_sort;
@@ -205,10 +204,12 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) =
       (* SProp primitive records are OK, if we squash and become fakerecord also OK *)
       if isrecord then univ_info
       (* 1 constructor with no arguments also OK in SProp (to make
-         things easier on ourselves when reducing we forbid letins) *)
+         things easier on ourselves when reducing we forbid letins)
+         unless ind_univ is sort polymorphic (for ease of implementation) *)
       else if (Environ.typing_flags env_ar_par).allow_uip
            && fst (splayed_lc.(0)) = []
            && List.for_all Context.Rel.Declaration.is_local_assum params
+           && Sorts.is_sprop univ_info.ind_univ
       then univ_info
       (* 1 constructor with arguments must squash if SProp
          (we could allow arguments in SProp but the reduction rule is a pain) *)
@@ -225,7 +226,7 @@ let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) =
 let check_record data =
   List.for_all (fun (_,(_,splayed_lc),info) ->
       (* records must have all projections definable -> equivalent to not being squashed *)
-      not info.ind_squashed
+      Option.is_empty info.ind_squashed
       (* relevant records must have at least 1 relevant argument,
          and we don't yet support variable relevance projections *)
       && (match info.record_arg_info with
@@ -326,7 +327,14 @@ let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
       RegularArity {mind_user_arity = arity; mind_sort = ind_univ}
   in
 
-  (arity,lc), (indices,splayed_lc), univ_info.ind_squashed
+  let squashed = Option.map (function
+      | AlwaysSquashed -> AlwaysSquashed
+      | SometimesSquashed qs ->
+        SometimesSquashed (List.map (UVars.subst_sort_level_quality usubst) qs))
+      univ_info.ind_squashed
+  in
+
+  (arity,lc), (indices,splayed_lc), squashed
 
 let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   let () = match mie.mind_entry_inds with
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 0603feca0f4d5..9a05a9352fd67 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -35,5 +35,5 @@ val typecheck_inductive : env -> sec_univs:UVars.Instance.t option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
-     bool (* squashed *))
+     squash_info option)
     array
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6e569c1bd85a8..2640c3bd6c7dd 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -304,14 +304,65 @@ let abstract_constructor_type_relatively_to_inductive_types_context ntyps mind t
 
 (* Get type of inductive, with parameters instantiated *)
 
+(* XXX questionable for sort poly inductives *)
 let inductive_sort_family mip =
   match mip.mind_arity with
   | RegularArity s -> Sorts.family s.mind_sort
   | TemplateArity _ -> Sorts.InType
 
-let elim_sort (_,mip) =
-  if not mip.mind_squashed then Sorts.InType
-  else inductive_sort_family mip
+let quality_leq q q' =
+  let open Sorts.Quality in
+  match q, q' with
+  | QVar q, QVar q' -> Sorts.QVar.equal q q'
+  | QConstant QSProp, _
+  | _, QConstant QType
+  | QConstant QProp, QConstant QProp
+    -> true
+
+  | (QVar _ | QConstant (QProp | QType)), _ -> false
+
+let is_squashed ((_,mip),u) =
+  match mip.mind_squashed with
+  | None -> None
+  | Some squash ->
+    let inds = match mip.mind_arity with
+      | TemplateArity _ -> assert false (* template is never squashed *)
+      | RegularArity a -> a.mind_sort
+    in
+    let inds = UVars.subst_instance_sort u inds in
+    match squash with
+    | AlwaysSquashed -> Some inds
+    | SometimesSquashed squash ->
+      match inds with
+      | Sorts.Set ->
+        (* impredicative set squashes are always AlwaysSquashed *)
+        assert false
+      | Sorts.Type _ -> None
+      | _ ->
+        let squash = List.map (UVars.subst_instance_quality u) squash in
+        if List.for_all (fun q -> quality_leq q (Sorts.quality inds)) squash then None
+        else Some inds
+
+let is_allowed_elimination specifu s =
+  match is_squashed specifu with
+  | None -> true
+  | Some inds ->
+    let open Sorts in
+    match s, inds with
+    (* impredicative set squash *)
+    | (SProp|Prop|Set), Set -> true
+    | (QSort _|Type _), Set -> false
+
+    (* we never squash to Type *)
+    | _, Type _ -> assert false
+
+    (* other squashes *)
+    | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true
+    | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq
+    | (Set|Type _), (SProp|Prop|QSort _) -> false
+    | Prop, SProp
+    | Prop, QSort _
+    | QSort _, (Prop|SProp) -> false
 
 let is_private (mib,_) = mib.mind_private = Some true
 let is_primitive_record (mib,_) =
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index bd7bca786ef5c..a8fb8ebf6bfb4 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -64,7 +64,14 @@ val type_of_inductive : mind_specif puniverses -> types
 val type_of_inductive_knowing_parameters :
   ?polyprop:bool -> mind_specif puniverses -> param_univs -> types
 
-val elim_sort : mind_specif -> Sorts.family
+val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool
+(** For squashing. *)
+
+val is_squashed : mind_specif puniverses -> Sorts.t option
+(** Returns the sort to which the inductive is squashed (i.e. the sort
+    of the inductive) if it is squashed. *)
+
+val is_allowed_elimination : mind_specif puniverses -> Sorts.t -> bool
 
 val is_private : mind_specif -> bool
 val is_primitive_record : mind_specif -> bool
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8539d6a83af9a..90f6d6770eea4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -114,6 +114,11 @@ let check_variance error v1 v2 =
   | None, Some _ -> error (CumulativeStatusExpected true)
   | Some _, None -> error (CumulativeStatusExpected false)
 
+let squash_info_equal s1 s2 = match s1, s2 with
+  | AlwaysSquashed, AlwaysSquashed -> true
+  | SometimesSquashed s1, SometimesSquashed s2 -> List.equal Sorts.Quality.equal s1 s2
+  | (AlwaysSquashed | SometimesSquashed _), _ -> false
+
 (* for now we do not allow reorderings *)
 
 let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 reso1 reso2=
@@ -139,7 +144,8 @@ let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 r
     let check f test why = if not (test (f p1) (f p2)) then error why in
       check (fun p -> p.mind_consnames) (Array.equal Id.equal) NotSameConstructorNamesField;
       check (fun p -> p.mind_typename) Id.equal NotSameInductiveNameInBlockField;
-      check (fun p -> p.mind_squashed) Bool.equal (NotConvertibleInductiveField p2.mind_typename);
+      check (fun p -> p.mind_squashed) (Option.equal squash_info_equal)
+        (NotConvertibleInductiveField p2.mind_typename);
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 88542fb935ed7..1290b4f738c0e 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -56,7 +56,7 @@ type ('constr, 'types) ptype_error =
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * GlobRef.t
   | ElimArity of pinductive * 'constr *
-    (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option
+    (('constr, 'types) punsafe_judgment * Sorts.t) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | CaseOnPrivateInd of inductive
   | WrongCaseInfo of pinductive * case_info
@@ -214,7 +214,7 @@ let map_ptype_error f = function
 | NotAType j -> NotAType (on_judgment f j)
 | BadAssumption j -> BadAssumption (on_judgment f j)
 | ElimArity (pi, c, ar) ->
-  ElimArity (pi, f c, Option.map (fun (j, s1, s2) -> (on_judgment f j, s1, s2)) ar)
+  ElimArity (pi, f c, Option.map (fun (j, s1) -> (on_judgment f j, s1)) ar)
 | CaseNotInductive j -> CaseNotInductive (on_judgment f j)
 | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
 | NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index e28f5c3285460..b4c99bebf66be 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -58,7 +58,7 @@ type ('constr, 'types) ptype_error =
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * GlobRef.t
   | ElimArity of pinductive * 'constr *
-      (('constr, 'types) punsafe_judgment * Sorts.family * Sorts.family) option
+      (('constr, 'types) punsafe_judgment * Sorts.t) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | CaseOnPrivateInd of inductive
   | WrongCaseInfo of pinductive * case_info
@@ -120,7 +120,7 @@ val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
 
 val error_elim_arity :
   env -> pinductive -> constr ->
-    (unsafe_judgment * Sorts.family * Sorts.family) option -> 'a
+    (unsafe_judgment * Sorts.t) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 66ff11b6cdc02..47524baccbdf7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -550,13 +550,11 @@ let type_of_case env (mib, mip as specif) ci u pms (pctx, pnas, p, rp, pt) iv c
     if not (is_inversion = should_invert_case env rp ci)
     then error_bad_invert env
   in
-  let () =
-    let ksort = Sorts.family sp in
-    let s = elim_sort specif in
-    if not (Sorts.family_leq ksort s) then
-      let pj = make_judge (it_mkLambda_or_LetIn p pctx) (it_mkProd_or_LetIn pt pctx) in
-      let kinds = Some (pj, ksort, s) in
-      error_elim_arity env (ind, u') c kinds
+  let () = if not (is_allowed_elimination (specif,u) sp) then begin
+    let pj = make_judge (it_mkLambda_or_LetIn p pctx) (it_mkProd_or_LetIn pt pctx) in
+    let kinds = Some (pj, sp) in
+    error_elim_arity env (ind, u') c kinds
+  end
   in
   (* Check that the scrutinee has the right type *)
   let rslty = type_case_scrutinee env (mib, mip) (u', largs) u pms (pctx, p) c in
diff --git a/kernel/uVars.ml b/kernel/uVars.ml
index 1b03463ba8e90..21ebcc4f04052 100644
--- a/kernel/uVars.ml
+++ b/kernel/uVars.ml
@@ -237,7 +237,7 @@ let subst_instance_quality s l =
       | Some n -> (fst (Instance.to_array s)).(n)
       | None -> l
     end
-  | _ -> l
+  | Quality.QConstant _ -> l
 
 let subst_instance_instance s i =
   let qs, us = Instance.to_array i in
@@ -407,18 +407,23 @@ let subst_sort_level_instance (qsubst,usubst) i =
 let subst_univs_level_abstract_universe_context subst (inst, csts) =
   inst, subst_univs_level_constraints subst csts
 
-let subst_fn_of_qsubst qsubst qv =
+let subst_sort_level_qvar (qsubst,_) qv =
   match Sorts.QVar.Map.find_opt qv qsubst with
   | None -> Quality.QVar qv
   | Some q -> q
 
-let subst_sort_level_sort (qsubst,usubst) s =
-  let fq qv = subst_fn_of_qsubst qsubst qv in
+let subst_sort_level_quality subst = function
+  | Sorts.Quality.QConstant _ as q -> q
+  | Sorts.Quality.QVar q ->
+    subst_sort_level_qvar subst q
+
+let subst_sort_level_sort (_,usubst as subst) s =
+  let fq qv = subst_sort_level_qvar subst qv in
   let fu u = subst_univs_level_universe usubst u in
   Sorts.subst_fn (fq,fu) s
 
-let subst_sort_level_relevance (qsubst,_) r =
-  Sorts.relevance_subst_fn (subst_fn_of_qsubst qsubst) r
+let subst_sort_level_relevance subst r =
+  Sorts.relevance_subst_fn (subst_sort_level_qvar subst) r
 
 let make_instance_subst i =
   let qarr, uarr = Instance.to_array i in
diff --git a/kernel/uVars.mli b/kernel/uVars.mli
index fdb6808931aa3..76f9878f20121 100644
--- a/kernel/uVars.mli
+++ b/kernel/uVars.mli
@@ -204,6 +204,8 @@ val subst_univs_level_abstract_universe_context :
 val subst_sort_level_instance : sort_level_subst -> Instance.t -> Instance.t
 (** Level to universe substitutions. *)
 
+val subst_sort_level_quality : sort_level_subst -> Sorts.Quality.t -> Sorts.Quality.t
+
 val subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t
 
 val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.relevance
@@ -211,6 +213,7 @@ val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.re
 (** Substitution of instances *)
 val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
 val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
+val subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t
 val subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t
 val subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0f83314d922b8..744fb558f4772 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2093,7 +2093,7 @@ let expected_elimination_sort env tomatchl =
       match tm with
       | IsInd (_,IndType(indf,_),_) ->
         (* Not a degenerated line, see coerce_to_indtype *)
-        let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in
+        let s' = Inductiveops.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in
         if Sorts.family_leq s s' then s else s'
       | NotInd _ -> s) tomatchl Sorts.InType
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c3395038ab5b3..7cd5eb730080b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -230,12 +230,70 @@ let inductive_has_local_defs env ind =
   let l2 = mib.mind_nparams + mip.mind_nrealargs in
   not (Int.equal l1 l2)
 
+let is_squashed sigma ((_,mip),u) =
+  match mip.mind_squashed with
+  | None -> None
+  | Some squash ->
+    let inds = match mip.mind_arity with
+      | TemplateArity _ -> assert false (* template is never squashed *)
+      | RegularArity a -> a.mind_sort
+    in
+    let inds = UVars.subst_instance_sort u inds in
+    match squash with
+    | AlwaysSquashed -> Some (EConstr.ESorts.make inds)
+    | SometimesSquashed squash ->
+      match inds with
+      | Sorts.Set ->
+        (* impredicative set squashes are always AlwaysSquashed *)
+        assert false
+      | Sorts.Type _ -> None
+      | _ ->
+        let squash = List.map (UVars.subst_instance_quality u) squash in
+        let nfq q = UState.nf_quality (Evd.evar_universe_context sigma) q in
+        let indq = nfq (Sorts.quality inds) in
+        if List.for_all (fun q -> Inductive.quality_leq (nfq q) indq) squash then None
+        else Some (EConstr.ESorts.make inds)
+
+let is_allowed_elimination sigma specifu s =
+  match is_squashed sigma specifu with
+  | None -> true
+  | Some inds ->
+    match EConstr.ESorts.kind sigma s, EConstr.ESorts.kind sigma inds with
+    (* impredicative set squash *)
+    | (SProp|Prop|Set), Set -> true
+    | (QSort _|Type _), Set -> false
+
+    (* we never squash to Type *)
+    | _, Type _ -> assert false
+
+    (* other squashes *)
+    | SProp, (SProp|Prop|QSort _) | Prop, Prop -> true
+    | QSort (q,_), QSort (indq,_) -> Sorts.QVar.equal q indq
+    | (Set|Type _), (SProp|Prop|QSort _) -> false
+    | Prop, QSort _ (* XXX check above_prop in the ustate? *)
+    | Prop, SProp
+    | QSort _, (Prop|SProp) -> false
+
+let elim_sort (_,mip) =
+  if Option.is_empty mip.mind_squashed then Sorts.InType
+  else Inductive.inductive_sort_family mip
+
 let top_allowed_sort env (kn,i as ind) =
   let specif = Inductive.lookup_mind_specif env ind in
-  Inductive.elim_sort specif
+  elim_sort specif
 
 let sorts_below top =
-  List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType]
+  List.filter (fun s ->
+      Sorts.family_equal s top
+      || match s, top with
+      | InSProp, _ -> true
+      | InProp, InSet -> true
+      | _, InType -> true
+      | (InProp|InSet|InType|InQSort), _ -> false)
+    Sorts.[InSProp;InProp;InSet;InType]
+
+let sorts_for_schemes specif =
+  sorts_below (elim_sort specif)
 
 let has_dependent_elim (mib,mip) =
   match mib.mind_record with
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 4668ee4955548..cde51223981dc 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -123,6 +123,12 @@ val inductive_has_local_defs : env -> inductive -> bool
 
 val sorts_below : Sorts.family -> Sorts.family list
 
+val sorts_for_schemes : mind_specif -> Sorts.family list
+
+val is_allowed_elimination : evar_map -> (mind_specif * UVars.Instance.t) -> EConstr.ESorts.t -> bool
+
+val elim_sort : mind_specif -> Sorts.family
+
 val top_allowed_sort : env -> inductive -> Sorts.family
 
 (** (Co)Inductive records with primitive projections do not have eta-conversion,
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index e984644492ebb..9244fff1577af 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -119,6 +119,8 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys =
     (env, sigma, IllTypedRecBody (i, na, jl, tys))
 
 let error_elim_arity ?loc env sigma pi c a =
+  (* XXX type_errors should have a 'sort type parameter *)
+  let a = Option.map (fun (x,s) -> x, EConstr.Unsafe.to_sorts s) a in
   raise_type_error ?loc
     (env, sigma, ElimArity (pi, c, a))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 69a3bfef0b338..374d86bf092f3 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -116,7 +116,7 @@ val error_ill_typed_rec_body :
 val error_elim_arity :
   ?loc:Loc.t -> env -> Evd.evar_map ->
       pinductive -> constr ->
-      (unsafe_judgment * Sorts.family * Sorts.family) option -> 'b
+      (unsafe_judgment * ESorts.t) option -> 'b
 
 val error_not_a_type :
   ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 66dad388ad808..b75cd80efe3e7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -258,21 +258,16 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let specif = lookup_mind_specif env (fst ind) in
-  let sorts = elim_sort specif in
   let pj = Retyping.get_judgment_of env sigma p in
   let _, s = whd_decompose_prod env sigma pj.uj_type in
   let sort =  match EConstr.kind sigma s with
-    | Sort s -> EConstr.ESorts.kind sigma s
+    | Sort s -> s
     | _ -> error_elim_arity env sigma ind c None
   in
-  let ksort = match Sorts.family sort with
-    | InType | InSProp | InSet | InProp as f -> f
-    | InQSort -> InType (* FIXME *)
-  in
-  if not (Sorts.family_leq ksort sorts) then
-    error_elim_arity env sigma ind c (Some (pj, ksort, sorts))
+  if Inductiveops.is_allowed_elimination sigma (specif,(snd ind)) sort then
+    ESorts.relevance_of_sort sigma sort
   else
-    Sorts.relevance_of_sort sort
+    error_elim_arity env sigma ind c (Some (pj, sort))
 
 let check_actual_type env sigma cj t =
   try Evarconv.unify_leq_delay env sigma cj.uj_type t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1ce6e55c6328c..051bf3e3d8aee 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1710,7 +1710,7 @@ let make_projection env sigma params cstr sign elim i n c (ind, u) =
         let (_, mip) as specif = Inductive.lookup_mind_specif env ind in
         let t = lift (i + 1 - n) t in
         let ksort = Retyping.get_sort_family_of (push_rel_context sign env) sigma t in
-        if Sorts.family_leq ksort (Inductive.elim_sort specif) then
+        if Sorts.family_leq ksort (Inductiveops.elim_sort specif) then
           let arity = List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt in
           let mknas ctx = Array.of_list (List.rev_map get_annot ctx) in
           let ci = Inductiveops.make_case_info env ind RegularStyle in
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b0ed957482736..8198074fcd780 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -334,7 +334,7 @@ let type_of_constant cb = cb.Declarations.const_type
 
 let uses_uip mib =
   Array.exists (fun mip ->
-      not mip.mind_squashed
+      Option.is_empty mip.mind_squashed
       && mip.mind_relevance == Sorts.Irrelevant
       && Array.length mip.mind_nf_lc = 1
       && List.length (fst mip.mind_nf_lc.(0)) = List.length mib.mind_params_ctxt)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 367f94db6ccf3..a63ff4d6fab0b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -835,7 +835,7 @@ let build_beq_scheme env handle kn =
       | Finite when truly_recursive || nb_ind > 1 (* Hum... *) ->
          let cores = Array.init nb_ind make_one_eq in
          Array.init nb_ind (fun i ->
-            let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
+            let kelim = Inductiveops.elim_sort (mib,mib.mind_packets.(i)) in
             if not (Sorts.family_leq InSet kelim) then
               raise (NonSingletonProp (kn,i));
             let decrArg = Context.Rel.length nonrecparams_ctx_with_eqs in
@@ -845,7 +845,7 @@ let build_beq_scheme env handle kn =
          assert (Int.equal nb_ind 1);
          (* If the inductive type is not recursive, the fixpoint is
              not used, so let's replace it with garbage *)
-         let kelim = Inductive.elim_sort (mib,mib.mind_packets.(0)) in
+         let kelim = Inductiveops.elim_sort (mib,mib.mind_packets.(0)) in
          if not (Sorts.family_leq InSet kelim) then raise (NonSingletonProp (kn,0));
          [|Term.it_mkLambda_or_LetIn (make_one_eq 0) recparams_ctx_with_eqs|]
   in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index b09cb762fca58..9a56b03bd2761 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -236,7 +236,9 @@ let explain_elim_arity env sigma ind c okinds =
   let pi = pr_inductive env (fst ind) in
   let pc = pr_leconstr_env env sigma c in
   let msg = match okinds with
-  | Some (pj, kp, ki) ->
+  | Some (pj, sp) ->
+      let kp = Sorts.family sp in
+      let ki = Inductiveops.elim_sort (Inductive.lookup_mind_specif env (fst ind)) in
       let explanation = error_elim_explain kp ki in
       let sorts = Inductiveops.sorts_below ki in
       let pki = Sorts.pr_sort_family ki in
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index f0aa50f227649..9d271b3dbf667 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -16,3 +16,12 @@ val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_erro
 val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t
 
 val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t
+
+(* XXX add cases for SProp (and sort poly?) *)
+type arity_error =
+  | NonInformativeToInformative
+  | StrongEliminationOnNonSmallType
+  | WrongArity
+
+val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
+(** Second argument is the familty of the inductive. *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index db5f870630093..fa7f8574b8fbd 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -204,7 +204,7 @@ let declare_one_case_analysis_scheme ?loc ind =
     else if not (Inductiveops.has_dependent_elim specif) then
       case_scheme_kind_from_type
     else case_dep_scheme_kind_from_type in
-  let kelim = Inductive.elim_sort (mib,mip) in
+  let kelim = Inductiveops.elim_sort (mib,mip) in
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        appropriate type *)
@@ -236,7 +236,7 @@ let declare_one_induction_scheme ?loc ind =
   let kind = Inductive.inductive_sort_family mip in
   let from_prop = kind == InProp in
   let depelim = Inductiveops.has_dependent_elim specif in
-  let kelim = Inductiveops.sorts_below (Inductive.elim_sort (mib,mip)) in
+  let kelim = Inductiveops.sorts_below (Inductiveops.elim_sort (mib,mip)) in
   let kelim = if Global.sprop_allowed () then kelim
     else List.filter (fun s -> s <> InSProp) kelim
   in
diff --git a/vernac/record.ml b/vernac/record.ml
index cd06859fec060..2c5bf718f2496 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -294,18 +294,24 @@ let warning_or_error ~info flags indsp err =
            prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++
            strbrk " not defined.")
     | BadTypedProj (fi,_ctx,te) ->
-        match te with
-          | ElimArity (_, _, Some (_, (InType | InSet), InProp)) ->
+      let err = match te with
+        | ElimArity (_, _, Some (_, s)) ->
+          Himsg.error_elim_explain (Sorts.family s)
+            (Inductiveops.elim_sort (Global.lookup_inductive indsp))
+        | _ -> WrongArity
+      in
+        match err with
+          | NonInformativeToInformative ->
               (Id.print fi ++
                 strbrk" cannot be defined because it is informative and " ++
                 Printer.pr_inductive (Global.env()) indsp ++
                 strbrk " is not.")
-          | ElimArity (_, _, Some (_, InType, InSet)) ->
+          | StrongEliminationOnNonSmallType ->
               (Id.print fi ++
                 strbrk" cannot be defined because it is large and " ++
                 Printer.pr_inductive (Global.env()) indsp ++
                 strbrk " is not.")
-          | _ ->
+          | WrongArity ->
               (Id.print fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if flags.Data.pf_coercion || flags.Data.pf_instance then user_err ~info st;