diff --git a/dev/ci/user-overlays/21417-mattam82-elab-elim-constraints.sh b/dev/ci/user-overlays/21417-mattam82-elab-elim-constraints.sh
new file mode 100644
index 000000000000..961b8dfcc5c8
--- /dev/null
+++ b/dev/ci/user-overlays/21417-mattam82-elab-elim-constraints.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/mattam82/coq-elpi elab-elim-constraints 21417
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index d3742b541384..8a53f90aee75 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -73,6 +73,7 @@ install_printer Top_printers.pperelevance
 install_printer Top_printers.ppqvar
 install_printer Top_printers.ppuni_level
 install_printer Top_printers.ppqvarset
+install_printer Top_printers.ppqset
 install_printer Top_printers.ppuniverse_set
 install_printer Top_printers.ppuniverse_instance
 install_printer Top_printers.ppuniverse_einstance
@@ -90,6 +91,7 @@ install_printer Top_printers.ppuniverseconstraints
 install_printer Top_printers.ppuniverse_context_future
 install_printer Top_printers.ppuniverses
 install_printer Top_printers.ppqualities
+install_printer Top_printers.ppelim_constraints
 install_printer Top_printers.pp_partialfsubst
 install_printer Top_printers.pp_partialsubst
 install_printer Top_printers.ppnamedcontextval
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 04e9dd5cc81e..ce63fd9e216a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -290,6 +290,7 @@ let pperelevance r = pprelevance (EConstr.Unsafe.to_relevance r)
 let prlev l = UnivNames.pr_level_with_global_universes l
 let prqvar q = UnivNames.pr_quality_with_global_universes q
 let ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc prqvar (QVar.Set.elements l) ++ str "}"))
+let ppqset qs = pp (hov 1 (str "{" ++ prlist_with_sep spc (Quality.pr prqvar) (Quality.Set.elements qs) ++ str "}"))
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
 let ppuniverse_einstance l = ppuniverse_instance (EConstr.Unsafe.to_instance l)
@@ -308,6 +309,7 @@ let ppuniverse_context_future c =
     ppuniverse_context ctx
 let ppuniverses u = pp (UGraph.pr_universes Level.raw_pr (UGraph.repr u))
 let ppqualities q = pp (QGraph.pr_qualities Quality.raw_pr q)
+let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr prqvar cstrs)
 let ppnamedcontextval e =
   let env = Global.env () in
   let sigma = Evd.from_env env in
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index bd3035169c3e..3d1791a2e798 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -154,6 +154,7 @@ val ppesorts : EConstr.ESorts.t -> unit
 val pperelevance : EConstr.ERelevance.t -> unit
 val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
 val ppqvarset : Sorts.QVar.Set.t -> unit
+val ppqset : Sorts.Quality.Set.t -> unit
 val ppuniverse_set : Univ.Level.Set.t -> unit
 val ppuniverse_instance : UVars.Instance.t -> unit
 val ppuniverse_einstance : EConstr.EInstance.t -> unit
@@ -171,6 +172,7 @@ val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : UVars.UContext.t Future.computation -> unit
 val ppuniverses : UGraph.t -> unit
 val ppqualities : QGraph.t -> unit
+val ppelim_constraints : Sorts.ElimConstraints.t -> unit
 
 val pp_partialfsubst : (CClosure.fconstr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit
 val pp_partialsubst : (EConstr.constr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit
diff --git a/doc/changelog/02-specification-language/21417-elab-elim-constraints-Added.rst b/doc/changelog/02-specification-language/21417-elab-elim-constraints-Added.rst
new file mode 100644
index 000000000000..45aee2d0ea1c
--- /dev/null
+++ b/doc/changelog/02-specification-language/21417-elab-elim-constraints-Added.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  implicit elaboration of :ref:`elimination constraints <elim-constraints>`
+  (`#21417 <https://github.com/rocq-prover/rocq/pull/21417>`_,
+  by Tomas Diaz).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 08c1d9f426cb..400f40336e3e 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -855,14 +855,14 @@ witness these temporary variables.
 Sort polymorphic inductives may be declared when every instantiation
 is valid.
 
-Elimination at a given universe instance requires that elimination is
-allowed at every ground instantiation of the sort variables in the
-instance. Additionally if the output sort at the given universe
-instance is sort polymorphic, the return type of the elimination must
-be at the same quality. These restrictions ignore :flag:`Definitional
-UIP`.
+.. _elim-constraints:
 
-For instance
+Elimination of Sort-Polymorphic Inductives
+------------------------------------------
+
+Sort-polymorphic inductives follow rules for their elimination, both
+when the target sort is polymorphic or not. We illustrate the first case
+on the following example:
 
 .. rocqtop:: all reset
 
@@ -870,7 +870,7 @@ For instance
 
    Inductive Squash@{s;u} (A:Type@{s;u}) : Prop := squash (_:A).
 
-Elimination to `Prop` and `SProp` is always allowed, so `Squash_ind`
+Here, elimination to `Prop` and `SProp` is always allowed, so `Squash_ind`
 and `Squash_sind` are automatically defined.
 
 Elimination to `Type` is not allowed with variable `s`, because the
@@ -890,19 +890,94 @@ However elimination to `Type` or to a polymorphic sort with `s := Prop` is allow
      : forall s, P s
      := fun s => match s with squash _ x => H x end.
 
+In fact, for a given universe instance, elimination is allowed if:
+
+- it is allowed for every ground instantiation of the sort variables in the instance, or
+
+- the output sort at the given universe instance is sort polymorphic and
+  the return type of the elimination is at the same quality.
+
+For instance, for the following inductive, elimination is not allowed unless the target sort of
+the inductive matches the sort it is eliminated to.
+
+.. rocqtop:: all
+
+   Inductive sum@{sl sr s;ul ur} (A:Type@{sl;ul}) (B:Type@{sr;ur}) : Type@{s;max(ul,ur)} :=
+   | inl (_:A)
+   | inr (_:B).
+
+.. rocqtop:: none
+
+   Arguments inl {_ _} _.
+   Arguments inr {_ _} _.
+
+.. rocqtop:: all
+
+   Fail Definition sum_elim@{sl sr s s';ul ur u'|}
+     (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+     (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+     (v : sum@{sl sr s;ul ur} A B) : P v :=
+         match v with
+         | inl x => fl x
+         | inr y => fr y
+         end.
+
+As this greatly inhibits the possibilities of sort polymorphism, we have introduced *elimination
+constraints* to manage these cases. Here, the annotation `s -> s'` can be added
+to tell Rocq that the definition is allowed for *every* sorts `s`, `s'` such that `s` eliminates
+into `s'`.
+
+.. rocqtop:: all
+
+   Definition sum_elim@{sl sr s s';ul ur u'|s -> s'}
+     (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+     (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+     (v : sum@{sl sr s;ul ur} A B) : P v :=
+         match v with
+         | inl x => fl x
+         | inr y => fr y
+         end.
+
+It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and `Prop` or
+`Prop` and `SProp`, but cannot be instantiated to e.g., `Prop` and `Type` or `SProp` and
+`Prop`.
+
+.. rocqtop:: all
+
+   Check sum_elim@{_ _ Type Prop;_ _ _}.
+   Check sum_elim@{_ _ Prop SProp;_ _ _}.
+   Fail Check sum_elim@{_ _ Prop Type;_ _ _}.
+   Fail Check sum_elim@{_ _ SProp Prop;_ _ _}.
+
 .. note::
 
-   Since inductive types with sort polymorphic output may only be
-   polymorphically eliminated to the same sort quality, containers
-   such as sigma types may be better defined as primitive records (which
-   do not have this restriction) when possible.
+   As with universe level constraints, elimination constraints can be elaborated
+   automatically if the constraints are denoted extensible with `+` **or** if they
+   are totally omitted. For instance, the two following definitions are legal.
 
    .. rocqtop:: all
 
-      Set Primitive Projections.
-      Record sigma@{s;u v} (A:Type@{s;u}) (B:A -> Type@{s;v})
-        : Type@{s;max(u,v)}
-        := pair { pr1 : A; pr2 : B pr1 }.
+      Definition sum_elim_ext@{sl sr s s';ul ur u'|+}
+        (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+        (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+        (v : sum@{sl sr s;ul ur} A B) : P v :=
+            match v with
+                | inl x => fl x
+                | inr y => fr y
+                end.
+
+      Definition sum_elim_elab@{sl sr s s';ul ur u'}
+        (A:Type@{sl;ul}) (B:Type@{sr;ur}) (P:sum@{sl sr s;ul ur} A B -> Type@{s';u'})
+        (fl : forall (x : A), P (inl x)) (fr : forall (y : B), P (inr y))
+        (v : sum@{sl sr s;ul ur} A B) : P v :=
+            match v with
+                | inl x => fl x
+                | inr y => fr y
+                end.
+
+.. note::
+
+    These restrictions ignore :flag:`Definitional UIP`.
 
 .. flag:: Printing Sort Qualities
 
@@ -915,7 +990,8 @@ However elimination to `Type` or to a polymorphic sort with `s := Prop` is allow
 Explicit Sorts
 ---------------
 
-Similar to universes, fresh global sorts can be declared with the :cmd:`Sort`.
+Similar to universes, fresh global sorts can be declared with the :cmd:`Sort`, and elimination
+constraint on global sorts can be declared with the :cmd:`Constraint`.
 
 .. cmd:: Sort {+ @ident }
          Sorts {+ @ident }
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index cbf8d8278a87..3a485da1e3fd 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -331,6 +331,8 @@ val whd_evar : Evd.evar_map -> constr -> constr
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
 val eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
+(** Does not produce QLeq nor QElimTo constraints *)
+
 val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
 val eq_existential : Evd.evar_map ->  (t -> t -> bool) -> existential -> existential -> bool
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 86fd3def5e96..89be5a976eee 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1176,6 +1176,9 @@ let set_above_prop evd q =
   add_constraints evd @@
     UnivProblem.Set.singleton (QLeq (Sorts.Quality.qprop, q))
 
+let set_elim_to evd q1 q2 =
+  add_constraints evd @@ UnivProblem.Set.singleton (QElimTo (q1, q2))
+
 let check_eq evd s s' =
   let quals = elim_graph evd in
   let ustate = evd.universes in
diff --git a/engine/evd.mli b/engine/evd.mli
index b08f6ca282e7..afdc2962d097 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -597,6 +597,7 @@ val set_eq_instances : ?flex:bool ->
   evar_map -> einstance -> einstance -> evar_map
 
 val set_eq_qualities : evar_map -> Sorts.Quality.t -> Sorts.Quality.t -> evar_map
+val set_elim_to : evar_map -> Sorts.Quality.t -> Sorts.Quality.t -> evar_map
 val set_above_prop : evar_map -> Sorts.Quality.t -> evar_map
 
 val check_eq : evar_map -> esorts -> esorts -> bool
diff --git a/engine/uState.ml b/engine/uState.ml
index 510d215aab85..0a4c951e23b7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -284,10 +284,12 @@ let collapse ?(except=QSet.empty) m =
 
 let pr prqvar_opt ({ qmap; elims; rigid } as m) =
   let open Pp in
+  (* Print the QVar using its name if any, e.g. "α1" or "s" *)
   let prqvar q = match prqvar_opt q with
     | None -> QVar.raw_pr q
     | Some qid -> Libnames.pr_qualid qid
   in
+  (* Print the "body" of the QVar, e.g. "α1 := Type", "α2 >= Prop" *)
   let prbody u = function
   | None ->
     if is_above_prop m u then str " >= Prop"
@@ -298,12 +300,15 @@ let pr prqvar_opt ({ qmap; elims; rigid } as m) =
     let q = Quality.pr prqvar q in
     str " := " ++ q
   in
+  (* Print the "name" (given by the user) of the Qvar, e.g. "(named s)" *)
   let prqvar_name q =
     match prqvar_opt q with
-    | None -> mt()
+    | None -> mt ()
     | Some qid -> str " (named " ++ Libnames.pr_qualid qid ++ str ")"
   in
-  h (prlist_with_sep fnl (fun (u, v) -> QVar.raw_pr u ++ prbody u v ++ prqvar_name u) (QMap.bindings qmap))
+  let prqvar_full (q1, q2) = QVar.raw_pr q1 ++ prbody q1 q2 ++ prqvar_name q1 in
+  hov 0 (prlist_with_sep fnl prqvar_full (QMap.bindings qmap) ++
+    str " |=" ++ brk (1, 2) ++ hov 0 (QGraph.pr_qualities (Quality.pr prqvar) elims))
 
 let elims m = m.elims
 
@@ -703,6 +708,7 @@ let process_constraints uctx cstrs =
     Sorts.subst_fn ((qnormalize sorts), subst_univs_universe normalize) s
   in
   let nf_constraint sorts = function
+    | QElimTo (a, b) -> QElimTo (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | QLeq (a, b) -> QLeq (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | QEq (a, b) -> QEq (Quality.subst (qnormalize sorts) a, Quality.subst (qnormalize sorts) b)
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
@@ -787,6 +793,7 @@ let process_constraints uctx cstrs =
       match cst with
     | QEq (a, b) -> unify_quality univs CONV (mk a) (mk b) local
     | QLeq (a, b) -> unify_quality univs CUMUL (mk a) (mk b) local
+    | QElimTo (a, b) -> { local with local_cst = PConstraints.add_quality (a, ElimTo, b) local.local_cst }
     | ULe (l, r) ->
       let local = unify_quality univs CUMUL l r local in
       let l = normalize_sort local.local_sorts l in
@@ -902,20 +909,22 @@ let problem_of_univ_constraints cstrs =
       in UnivProblem.Set.add cstr' acc)
     cstrs UnivProblem.Set.empty
 
+let problem_of_elim_constraints cstrs =
+  ElimConstraints.fold (fun (l, k, r) pbs ->
+      let open ElimConstraint in
+      match k with
+      | ElimTo -> UnivProblem.Set.add (QElimTo (l, r)) pbs
+      | Equal -> UnivProblem.Set.add (QEq (l, r)) pbs)
+    cstrs UnivProblem.Set.empty
+
 let add_univ_constraints uctx cstrs =
   let cstrs = problem_of_univ_constraints cstrs in
   add_constraints ~src:Static uctx cstrs
 
 let add_poly_constraints ?src uctx (qcstrs, ucstrs) =
-  let ucstrs = problem_of_univ_constraints ucstrs in
-  (* XXX when elimination constraints become available in unification we should
-     rely on it rather than playing this little dance *)
-  let fold (s1, pb, s2) (qeq, qelm) = match pb with
-  | ElimConstraint.ElimTo -> (qeq, ElimConstraints.add (s1, pb, s2) qelm)
-  | ElimConstraint.Equal -> (UnivProblem.Set.add (QEq (s1, s2)) qeq, qelm)
-  in
-  let qeq, qcstrs = ElimConstraints.fold fold qcstrs (UnivProblem.Set.empty, ElimConstraints.empty) in
-  let uctx = add_constraints ?src uctx (UnivProblem.Set.union ucstrs qeq) in
+  let lvl_pbs = problem_of_univ_constraints ucstrs in
+  let elim_pbs = problem_of_elim_constraints qcstrs in
+  let uctx = add_constraints ?src uctx (UnivProblem.Set.union lvl_pbs elim_pbs) in
   let local = on_snd (fun cst -> PConstraints.union cst (PConstraints.of_qualities qcstrs)) uctx.local in
   let sort_variables = QState.merge_constraints (fun cst -> merge_elim_constraints ?src uctx qcstrs cst) uctx.sort_variables in
   { uctx with local; sort_variables }
@@ -945,6 +954,10 @@ let check_constraint uctx (c:UnivProblem.t) =
         | QConstant QProp, QVar q -> QState.is_above_prop uctx.sort_variables q
         | (QConstant _ | QVar _), _ -> false
       end
+  | QElimTo (a, b) ->
+    let a = nf_quality uctx a in
+    let b = nf_quality uctx b in
+    Inductive.eliminates_to (QState.elims uctx.sort_variables) a b
   | ULe (u,v) -> UGraph.check_leq_sort (elim_graph uctx) uctx.universes u v
   | UEq (u,v) -> UGraph.check_eq_sort (elim_graph uctx) uctx.universes u v
   | ULub (u,v) -> UGraph.check_eq_level uctx.universes u v
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 0fd170e199d8..4bfccc5ac207 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -14,6 +14,7 @@ open Sorts
 type t =
   | QEq of Quality.t * Quality.t
   | QLeq of Quality.t * Quality.t
+  | QElimTo of Quality.t * Quality.t
   | ULe of Sorts.t * Sorts.t
   | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t
@@ -21,12 +22,13 @@ type t =
 
 let is_trivial = function
   | QLeq (a,b) -> Inductive.raw_eliminates_to a b
+  | QElimTo (a, b) -> Inductive.raw_eliminates_to a b
   | QEq (a, b) -> Quality.equal a b
   | ULe (u, v) | UEq (u, v) -> Sorts.equal u v
   | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
 let force = function
-  | QEq _ | QLeq _ | ULe _ | UEq _ | UWeak _ as cst -> cst
+  | QEq _ | QElimTo _ | QLeq _ | ULe _ | UEq _ | UWeak _ as cst -> cst
   | ULub (u,v) -> UEq (Sorts.sort_of_univ @@ Universe.make u, Sorts.sort_of_univ @@ Universe.make v)
 
 let check_eq_level g u v = UGraph.check_eq_level g u v
@@ -37,12 +39,15 @@ module Set = struct
     type nonrec t = t
 
     let compare x y =
-      match x, y with
-      | (QEq (a, b) | QLeq (a, b)),
-        (QEq (a', b') | QLeq (a', b')) ->
+      let compare_qualities (a, b) (a', b') =
         let i = Quality.compare a a' in
         if i <> 0 then i
         else Quality.compare b b'
+      in
+      match x, y with
+      | QEq (a, b), QEq (a', b')
+      | QLeq (a, b), QLeq (a', b')
+      | QElimTo (a, b), QElimTo (a', b') -> compare_qualities (a, b) (a', b')
       | ULe (u, v), ULe (u', v') ->
         let i = Sorts.compare u u' in
         if Int.equal i 0 then Sorts.compare v v'
@@ -61,6 +66,8 @@ module Set = struct
       | _, QEq _ -> 1
       | QLeq _, _ -> -1
       | _, QLeq _ -> 1
+      | QElimTo _, _ -> -1
+      | _, QElimTo _ -> 1
       | ULe _, _ -> -1
       | _, ULe _ -> 1
       | UEq _, _ -> -1
@@ -78,6 +85,7 @@ module Set = struct
   let pr_one = let open Pp in function
     | QEq (a, b) -> Quality.raw_pr a ++ str " = " ++ Quality.raw_pr b
     | QLeq (a, b) -> Quality.raw_pr a ++ str " <= " ++ Quality.raw_pr b
+    | QElimTo (a, b) -> Quality.raw_pr a ++ str " -> " ++ Quality.raw_pr b
     | ULe (u, v) -> Sorts.debug_print u ++ str " <= " ++ Sorts.debug_print v
     | UEq (u, v) -> Sorts.debug_print u ++ str " = " ++ Sorts.debug_print v
     | ULub (u, v) -> Level.raw_pr u ++ str " /\\ " ++ Level.raw_pr v
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
index c71cdf078307..6f53d88c83b4 100644
--- a/engine/univProblem.mli
+++ b/engine/univProblem.mli
@@ -23,6 +23,7 @@ open UVars
 type t =
   | QEq of Sorts.Quality.t * Sorts.Quality.t
   | QLeq of Sorts.Quality.t * Sorts.Quality.t
+  | QElimTo of Sorts.Quality.t * Sorts.Quality.t
   | ULe of Sorts.t * Sorts.t
   | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t
diff --git a/kernel/pConstraints.ml b/kernel/pConstraints.ml
index 61578405224b..5c5a47c6e48b 100644
--- a/kernel/pConstraints.ml
+++ b/kernel/pConstraints.ml
@@ -61,9 +61,10 @@ let filter_univs f (qc, lc) =
 
 let pr prv prl (qc, lc) =
   let open Pp in
-  let ppelim = if ElimConstraints.is_empty qc then mt()
-               else ElimConstraints.pr prv qc ++ str"," in
-  v 0 (ppelim ++ UnivConstraints.pr prl lc)
+  let sep = if ElimConstraints.is_empty qc || UnivConstraints.is_empty lc
+            then mt ()
+            else pr_comma () in
+  v 0 (ElimConstraints.pr prv qc ++ sep ++ UnivConstraints.pr prl lc)
 
 module HPConstraints =
   Hashcons.Make(
diff --git a/kernel/qGraph.ml b/kernel/qGraph.ml
index c496f1ef5049..1f1a66398a2d 100644
--- a/kernel/qGraph.ml
+++ b/kernel/qGraph.ml
@@ -118,7 +118,8 @@ let enforce_func k =
   | ElimConstraint.Equal -> G.enforce_eq
 
 type elimination_error =
-  | IllegalConstraint
+  | IllegalConstraintFromSProp of Quality.t
+  | IllegalConstantConstraint of Quality.constant * Quality.constant
   | CreatesForbiddenPath of Quality.t * Quality.t
   | MultipleDominance of Quality.t * Quality.t * Quality.t
   | QualityInconsistency of quality_inconsistency
@@ -210,10 +211,13 @@ let check_rigid_paths g =
   | Some (q1, q2) -> raise (EliminationError (CreatesForbiddenPath (q1, q2)))
 
 let add_rigid_path q1 q2 g =
-  if (Quality.is_qconst q1 && Quality.is_qconst q2) || (Quality.is_qsprop q1 && not (Quality.is_qsprop q2)) then
-    raise (EliminationError IllegalConstraint)
-  else
-    { g with rigid_paths = RigidPaths.add_elim_to q1 q2 g.rigid_paths }
+  let open Quality in
+  match q1, q2 with
+  (* Adding a constraint from SProp -> * is not allowed *)
+  | QConstant QSProp, _ -> raise (EliminationError (IllegalConstraintFromSProp q2))
+  (* Adding constraints between constants is not allowed *)
+  | QConstant qc1, QConstant qc2 -> raise (EliminationError (IllegalConstantConstraint (qc1, qc2)))
+  | _, _ -> { g with rigid_paths = RigidPaths.add_elim_to q1 q2 g.rigid_paths }
 
 let enforce_constraint (q1, k, q2) g =
   match enforce_func k q1 q2 g.graph with
@@ -310,23 +314,23 @@ let is_empty g = QVar.Set.is_empty (qvar_domain g)
 (* Pretty printing *)
 
 let pr_pmap sep pr map =
-  let cmp (u,_) (v,_) = Quality.compare u v in
+  let cmp (q1, _) (q2, _) = Quality.compare q1 q2 in
   Pp.prlist_with_sep sep pr (List.sort cmp (Quality.Map.bindings map))
 
 let pr_arc prq =
   let open Pp in
   function
-  | u, G.Node ltle ->
+  | q1, G.Node ltle ->
     if Quality.Map.is_empty ltle then mt ()
     else
-      prq u ++ str " " ++
+      prq q1 ++ spc () ++
       v 0
-        (pr_pmap spc (fun (v, strict) ->
-              (if strict then str "< " else str "<= ") ++ prq v)
+        (pr_pmap spc (fun (q2, _) ->
+              str "-> " ++ prq q2)
             ltle) ++
       fnl ()
-  | u, G.Alias v ->
-    prq u  ++ str " = " ++ prq v ++ fnl ()
+  | q1, G.Alias q2 ->
+    prq q1  ++ str " <-> " ++ prq q2 ++ fnl ()
 
 let repr g = G.repr g.graph
 
@@ -340,8 +344,8 @@ let explain_quality_inconsistency prv r =
   let open Pp in
   let pr_cst = function
     | AcyclicGraph.Eq -> str"="
-    | AcyclicGraph.Le -> str"~>"
-    | AcyclicGraph.Lt -> str"~>" (* Yes, it's the same as above. *)
+    | AcyclicGraph.Le -> str"->"
+    | AcyclicGraph.Lt -> str"->" (* Yes, it's the same as above. *)
   in
   match r with
   | None -> mt()
@@ -355,18 +359,22 @@ let explain_quality_inconsistency prv r =
        str "because it would identify " ++
          pr_enum (Quality.pr prv) constants ++
          spc() ++ str"which is inconsistent." ++ spc() ++
-         str"This is introduced by the constraints" ++ spc() ++ Quality.pr prv pstart ++
-         prlist (fun (r,v) -> spc() ++ pr_cst r ++ str" " ++ Quality.pr prv v) p
+         str"This is introduced by the constraints " ++
+         prlist (fun (r, v) -> Quality.pr prv v ++ spc() ++ pr_cst r ++ spc()) p ++
+         Quality.pr prv pstart
 
 let explain_elimination_error defprv err =
   let open Pp in
   match err with
-  | IllegalConstraint -> str "A constraint involving two constants or SProp ~> s is illegal."
+  | IllegalConstraintFromSProp q -> str "Enforcing elimination constraints from SProp to any other sort is not allowed. " ++ brk (1, 0) ++
+    str "This expression would enforce that SProp eliminates to " ++ Quality.pr defprv q ++ str "."
+  | IllegalConstantConstraint (q1, q2) -> str "Enforcing elimination constraints between constant sorts (Type, Prop or SProp) is not allowed." ++ brk (1, 0) ++
+    str "Here: " ++ Quality.Constants.pr q1 ++ str" and " ++ Quality.Constants.pr q2 ++ str "."
   | CreatesForbiddenPath (q1,q2) ->
      str "This expression would enforce a non-declared elimination constraint between" ++
        spc() ++ Quality.pr defprv q1 ++ spc() ++ str"and" ++ spc() ++ Quality.pr defprv q2
   | MultipleDominance (q1,qv,q2) ->
-     let pr_elim q = Quality.pr defprv q ++ spc() ++ str"~>" ++ spc() ++ Quality.pr defprv qv in
+     let pr_elim q = Quality.pr defprv q ++ spc() ++ str"->" ++ spc() ++ Quality.pr defprv qv in
      str "This expression enforces" ++ spc() ++ pr_elim q1 ++ spc() ++ str"and" ++ spc() ++
        pr_elim q2 ++ spc() ++ str"which might make type-checking undecidable"
   | QualityInconsistency (prv, (k, q1, q2, r)) ->
diff --git a/kernel/qGraph.mli b/kernel/qGraph.mli
index 2f4c44e31334..41b72650fb28 100644
--- a/kernel/qGraph.mli
+++ b/kernel/qGraph.mli
@@ -35,7 +35,8 @@ type quality_inconsistency =
     (ElimConstraint.kind * Quality.t * Quality.t * explanation option)
 
 type elimination_error =
-  | IllegalConstraint
+  | IllegalConstraintFromSProp of Quality.t
+  | IllegalConstantConstraint of Quality.constant * Quality.constant
   | CreatesForbiddenPath of Quality.t * Quality.t
   | MultipleDominance of Quality.t * Quality.t * Quality.t
   | QualityInconsistency of quality_inconsistency
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index f95495183c76..29ad05e57a2a 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -316,7 +316,7 @@ module ElimConstraints = struct include Stdlib.Set.Make(ElimConstraint)
   let pr prq c =
     let open Pp in
     v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
-      hov 0 (Quality.pr prq u1 ++ ElimConstraint.pr_kind op ++ Quality.pr prq u2))
+      hov 0 (Quality.pr prq u1 ++ spc() ++ ElimConstraint.pr_kind op ++ spc() ++ Quality.pr prq u2))
        (elements c))
 
   module HConstraints = CSet.Hashcons(ElimConstraint)(struct
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index bf103fc7f2cc..57a3f09f4862 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2171,7 +2171,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty
       let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in
       let check_elim_sort sigma squash =
         try Inductiveops.squash_elim_sort sigma squash rtnsort
-        with UGraph.UniverseInconsistency _ ->
+        with QGraph.EliminationError _ | UGraph.UniverseInconsistency _ ->
           (* Incompatible constraints are ignored and handled later
              when typing the pattern-matching. *)
           sigma
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f2b7cbc659e5..0f9627834e7d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -283,20 +283,19 @@ let is_allowed_elimination sigma ((_,mip) as specif,u) s =
       s
 
 let make_allowed_elimination_actions sigma s =
-  Inductive.
-  { not_squashed = Some sigma
+  Inductive.{
+    not_squashed = Some sigma
   ; squashed_to_set_below = Some sigma
   ; squashed_to_set_above = (
     try Some (Evd.set_leq_sort sigma s ESorts.set)
     with UGraph.UniverseInconsistency _ -> None)
-  ; squashed_to_quality =
-      fun indq -> let sq = EConstr.ESorts.quality sigma s in
-               if Inductive.eliminates_to (Evd.elim_graph sigma) indq sq
-               then Some sigma
-               else
-                 let mk q = ESorts.make @@ Sorts.make q Univ.Universe.type0 in
-                 try Some (Evd.set_leq_sort sigma (mk sq) (mk indq))
-                 with UGraph.UniverseInconsistency _ -> None }
+  ; squashed_to_quality = fun indq ->
+      let sq = EConstr.ESorts.quality sigma s in
+      if Inductive.eliminates_to (Evd.elim_graph sigma) indq sq
+      then Some sigma
+      else
+        try Some (Evd.set_elim_to sigma indq sq)
+        with QGraph.EliminationError _ | UGraph.UniverseInconsistency _ -> None }
 
 let make_allowed_elimination sigma ((_,mip) as specif,u) s =
   match mip.mind_record with
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 8a80b6d82007..77ac9bd20506 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -449,7 +449,8 @@ let magically_constant_of_fixbody env sigma (reference, params) bd = function
             let addus l r (qs,us) = qs, Univ.Level.Map.add l r us in
             let subst = Set.fold (fun cst acc ->
                 match cst with
-                | QEq (a,b) | QLeq (a,b) ->
+                | QLeq _ | QElimTo _ -> assert false (* eq_constr_universes cannot produce QLeq nor QElimTo constraints *)
+                | QEq (a, b) ->
                   let a = match a with
                     | QVar q -> q
                     | _ -> assert false
diff --git a/test-suite/output/ShowUnivs.out b/test-suite/output/ShowUnivs.out
index 5f9492ca9e61..5d026d473e47 100644
--- a/test-suite/output/ShowUnivs.out
+++ b/test-suite/output/ShowUnivs.out
@@ -6,7 +6,10 @@ ALGEBRAIC UNIVERSES:
 FLEXIBLE UNIVERSES:
  
 SORTS:
- 
+  |= Prop -> SProp
+     Type -> Prop
+          -> SProp
+     
 WEAK CONSTRAINTS:
  
 
@@ -30,7 +33,14 @@ FLEXIBLE UNIVERSES:
 SORTS:
  α1 := Type
  α2 := Type
- α3 := α1
+ α3 := α1 |=
+   α1 <-> Type
+   α2 <-> Type
+   α3 <-> α1
+   Prop -> SProp
+   Type -> Prop
+        -> SProp
+   
 WEAK CONSTRAINTS:
  
 
diff --git a/test-suite/output/sort_poly_elim_error.out b/test-suite/output/sort_poly_elim_error.out
index cc194dfdf46d..a8eeffe15d22 100644
--- a/test-suite/output/sort_poly_elim_error.out
+++ b/test-suite/output/sort_poly_elim_error.out
@@ -6,14 +6,11 @@ the return type has sort "Type" while it should be SProp or Prop.
 Elimination of an inductive object of sort Prop
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs.
-File "./output/sort_poly_elim_error.v", line 19, characters 0-106:
+File "./output/sort_poly_elim_error.v", line 17, characters 0-106:
 The command has indeed failed with message:
-Incorrect elimination of "x" in the inductive type "sBox@{s s' ; u}":
-the return type has sort "Type@{s ; u}"
-while it should be in a sort s' eliminates to.
-Elimination of a sort polymorphic inductive object instantiated to a variable sort quality
-is only allowed on itself or with an explicit elimination constraint to the target sort.
-File "./output/sort_poly_elim_error.v", line 24, characters 0-37:
+Elimination constraints are not implied by the ones declared: 
+s' -> s
+File "./output/sort_poly_elim_error.v", line 23, characters 0-37:
 The command has indeed failed with message:
 Incorrect elimination of "sC" in the inductive type "sP":
 the return type has sort "Prop" while it should be SProp.
diff --git a/test-suite/output/sort_poly_elim_error.v b/test-suite/output/sort_poly_elim_error.v
index 0b54fd59340b..f2b493a1e6c5 100644
--- a/test-suite/output/sort_poly_elim_error.v
+++ b/test-suite/output/sort_poly_elim_error.v
@@ -7,10 +7,8 @@ Arguments inr {A B}.
 
 Fail Check (fun p : sum@{Prop;_ _} True False => match p return Set with inl a => unit | inr b => bool end).
 (*
-Error: Incorrect elimination of "p" in the inductive type "sum":
-the return type has sort "Type@{Set+1}" while it should be at some variable quality.
-Elimination of an inductive object of sort Type is not allowed on a predicate in sort Type
-because wrong arity.
+Error: The quality constraints are inconsistent: cannot enforce Prop -> Type because it would identify Type and Prop which is inconsistent.
+This is introduced by the constraints Prop -> Type
 *)
 
 
@@ -18,7 +16,12 @@ Inductive sBox@{s s';u|} (A:Type@{s;u}) : Type@{s';u} := sbox (_:A).
 
 Fail Definition elim@{s s';u|} (A:Type@{s;u}) (x:sBox@{s s';u} A) : A :=
   match x with sbox _ v => v end.
+(* Error: Elimination constraints are not implied by the ones declared: s' -> s *)
 
 Inductive sP : SProp := sC.
 
 Fail Check match sC with sC => I end.
+(*
+Error: The quality constraints are inconsistent: cannot enforce SProp -> Prop because it would identify Prop and SProp which is inconsistent.
+This is introduced by the constraints SProp -> Prop
+*)
diff --git a/test-suite/success/sort_poly.v b/test-suite/success/sort_poly.v
index 8bb4d81fb7a1..0b622b5abe55 100644
--- a/test-suite/success/sort_poly.v
+++ b/test-suite/success/sort_poly.v
@@ -103,8 +103,8 @@ Module Inductives.
   Inductive foo1@{s; |} : Type@{s;Set} := .
   Fail Check foo1_sind.
 
-  Fail Definition foo1_False@{s;+|+} (x:foo1@{s;}) : False := match x return False with end.
-  (* XXX error message is bad *)
+  Definition foo1_False@{s;+|+} (x:foo1@{s;}) : False := match x return False with end.
+  (* s ;  |= s -> Prop *)
 
   Inductive foo2@{s; |} := Foo2 : Type@{s;Set} -> foo2.
   Check foo2_rect.
@@ -124,6 +124,10 @@ Module Inductives.
     (f : foo5 A)
     : P f
     := match f with Foo5 _ a => H a end.
+    (*
+    Error: The quality constraints are inconsistent: cannot enforce Prop -> Type because it would identify Type and Prop which is inconsistent.
+    This is introduced by the constraints Prop -> Type
+    *)
 
   Definition foo5_Prop_rect (A:Prop) (P:foo5 A -> Type)
     (H : forall a, P (Foo5 A a))
@@ -135,18 +139,12 @@ Module Inductives.
   Inductive foo6@{s; |} : Type@{s;Set} := Foo6.
   Fail Check foo6_sind.
 
-  Fail Definition foo6_rect@{s;+|+} (P:foo6@{s;} -> Type)
-    (H : P Foo6)
-    (f : foo6)
-    : P f
-    := match f with Foo6 => H end.
-
-  (* implicit quality is set to Type *)
-  Definition foo6_rect (P:foo6 -> Type)
+  Definition foo6_rect@{s;+|+} (P:foo6@{s;} -> Type)
     (H : P Foo6)
     (f : foo6)
     : P f
     := match f with Foo6 => H end.
+  (* s ; u |= s -> Type *)
 
   Definition foo6_prop_rect (P:foo6 -> Type)
     (H : P Foo6)
@@ -249,14 +247,15 @@ Module Inductives.
   Definition pr2@{s;+|} {A B} (s:sigma@{s;_ _} A B) : B (pr1 s)
     := match s with pair _ _ _ y => y end.
 
-  (* but we can't prove eta *)
+  (* And we can prove eta with implicit elaboration of elimination constraints.
+    We can't prove eta without the constraints. *)
   Inductive seq@{s;u|} (A:Type@{s;u}) (a:A) : A -> Prop := seq_refl : seq A a a.
   Arguments seq_refl {_ _}.
 
   Definition eta@{s;+|+} A B (s:sigma@{s;_ _} A B) : seq _ s (pair A B (pr1 s) (pr2 s)).
   Proof.
-    Fail destruct s.
-  Abort.
+    destruct s. simpl. reflexivity.
+  Qed.
 
   (* sigma as a primitive record works better *)
   Record Rsigma@{s;u v|} (A:Type@{s;u}) (B:A -> Type@{s;v}) : Type@{s;max(u,v)}
diff --git a/test-suite/success/sort_poly_elab.v b/test-suite/success/sort_poly_elab.v
new file mode 100644
index 000000000000..015b61193f9b
--- /dev/null
+++ b/test-suite/success/sort_poly_elab.v
@@ -0,0 +1,175 @@
+Set Universe Polymorphism.
+
+Inductive sum@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) : Type@{s;max(ul,ur)} :=
+| inl : A -> sum A B
+| inr : B -> sum A B.
+
+Arguments inl {A B} _ , [A] B _.
+Arguments inr {A B} _ , A [B] _.
+
+(* Elimination constraint left explicitly empty. Definition fails because of missing constraint. *)
+Fail Definition sum_elim@{sl sr s0 s0';ul ur v|}
+  (A : Type@{sl;ul}) (B : Type@{sr;ur}) (P : sum@{sl sr s0;ul ur} A B -> Type@{s0';v})
+  (fl : forall a, P (inl a)) (fr : forall b, P (inr b)) (x : sum@{sl sr s0;ul ur} A B) :=
+    match x with
+    | inl a => fl a
+    | inr b => fr b
+    end.
+(* The command has indeed failed with message:
+Elimination constraints are not implied by the ones declared: s0->s0' *)
+
+(* Using + to elaborate missing constraints. Definition passes *)
+Definition sum_elim@{sl sr s0 s0';ul ur v|+}
+  (A : Type@{sl;ul}) (B : Type@{sr;ur}) (P : sum@{sl sr s0;ul ur} A B -> Type@{s0';v})
+  (fl : forall a, P (inl a)) (fr : forall b, P (inr b)) (x : sum@{sl sr s0;ul ur} A B) :=
+    match x with
+    | inl a => fl a
+    | inr b => fr b
+    end.
+(* sl sr s0 s0' ; ul ur v |= s0->s0' *)
+
+Definition sum_sind := sum_elim@{Type Type Type SProp;_ _ _}.
+Definition sum_rect := sum_elim@{Type Type Type Type;_ _ _}.
+Definition sum_ind := sum_elim@{Type Type Type Prop;_ _ _}.
+
+Definition or_ind := sum_elim@{Prop Prop Prop Prop;_ _ _}.
+Definition or_sind := sum_elim@{Prop Prop Prop SProp;_ _ _}.
+Fail Definition or_rect := sum_elim@{Prop Prop Prop Type;_ _ _}.
+(* The command has indeed failed with message:
+The quality constraints are inconsistent: cannot enforce Prop -> Type because it would identifyType and Prop which is inconsistent.
+This is introduced by the constraints Type -> Prop *)
+
+Definition sumor := sum@{Type Prop Type;_ _}.
+
+Definition sumor_sind := sum_elim@{Type Prop Type SProp;_ _ _}.
+Definition sumor_rect := sum_elim@{Type Prop Type Type;_ _ _}.
+Definition sumor_ind := sum_elim@{Type Prop Type Prop;_ _ _}.
+
+(* Implicit constraints are elaborated *)
+Definition idT@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+  : sum@{sl sr Type;ul ur} A B :=
+  match x return sum@{sl sr Type;ul ur} A B with
+  | inl a => inl a
+  | inr b => inr b
+  end.
+(* sl sr s ; ul ur |= s->Type *)
+
+(* Implicit constraints are elaborated *)
+Definition idP@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+  : sum@{sl sr Prop;ul ur} A B :=
+  match x return sum@{sl sr Prop;ul ur} A B with
+  | inl a => inl a
+  | inr b => inr b
+  end.
+(* sl sr s ; ul ur |= s->Prop *)
+
+(* Implicit constraints are elaborated *)
+Definition idS@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+  : sum@{sl sr SProp;ul ur} A B :=
+  match x return sum@{sl sr SProp;ul ur} A B with
+  | inl a => inl a
+  | inr b => inr b
+  end.
+(* sl sr s ; ul ur |= s->SProp *)
+
+(* Implicit constraints are elaborated *)
+Definition idV@{sl sr s s';ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+  : sum@{sl sr s';ul ur} A B :=
+  match x return sum@{sl sr s';ul ur} A B with
+  | inl a => inl a
+  | inr b => inr b
+  end.
+(* sl sr s s' ; ul ur |= s->s' *)
+
+Inductive List'@{s s';l} (A : Type@{s;l}) : Type@{s';l} :=
+| nil' : List' A
+| cons' : A -> List' A -> List' A.
+
+Arguments nil' {A}.
+Arguments cons' {A} _ _.
+
+Definition list'_elim@{s s0 s';l l'}
+  (A : Type@{s;l}) (P : List'@{s s0;l} A -> Type@{s';l'})
+  (fn : P nil') (fc : forall (x : A) (l : List' A), P l -> P (cons' x l)) :=
+  fix F (l : List'@{s s0;l} A) : P l :=
+    match l with
+    | nil' => fn
+    | cons' x l => fc x l (F l)
+    end.
+(* s s0 s' ; l l' |= s0->s' *)
+
+Fixpoint list'_idT@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Type;l} A :=
+  match l with
+  | nil' => nil'
+  | cons' x l => cons' x (list'_idT l)
+  end.
+(* s s' ; l |= s'->Type *)
+
+Fixpoint list'_idP@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Prop;l} A :=
+  match l with
+  | nil' => nil'
+  | cons' x l => cons' x (list'_idP l)
+  end.
+(* s s' ; l |= s'->Prop *)
+
+Fixpoint list'_idS@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s SProp;l} A :=
+  match l with
+  | nil' => nil'
+  | cons' x l => cons' x (list'_idS l)
+  end.
+(* s s' ; l |= s'->SProp *)
+
+(* Elimination constraint left explicitly empty. Definition fails because of missing constraint. *)
+Fail Fixpoint list'_idV@{s s0 s';l l'|l <= l'} {A : Type@{s;l}} (l : List'@{s s0;l} A) : List'@{s s';l'} A :=
+  match l with
+  | nil' => nil'
+  | cons' x l => cons' x (list'_idV l)
+  end.
+(* The command has indeed failed with message:
+Elimination constraints are not implied by the ones declared: s0->s' *)
+
+(* Using + to elaborate missing constraints. Definition passes *)
+Fixpoint list'_idV@{s s0 s';l l'|l <= l' + } {A : Type@{s;l}} (l : List'@{s s0;l} A) : List'@{s s';l'} A :=
+  match l with
+  | nil' => nil'
+  | cons' x l => cons' x (list'_idV l)
+  end.
+(* s s0 s' ; l l' |= s0->s', l <= l' *)
+
+
+Inductive False'@{s;u} : Type@{s;u} :=.
+
+Definition False'_False@{s; +|+} (x : False'@{s;_}) : False := match x return False with end.
+(* s ; u |= s->Prop *)
+
+Inductive bool@{s;u} : Type@{s;u} := true | false.
+
+Definition bool_to_Prop@{s;u} (b : bool@{s;u}) : Prop.
+Proof.
+  destruct b.
+  - exact True.
+  - exact False.
+Defined.
+(* s ; u |= s->Type *)
+
+Definition bool_to_True_conj@{s;u} (b : bool@{s;u}) : True \/ True.
+Proof.
+  destruct b.
+  - exact (or_introl I).
+  - exact (or_intror I).
+Defined.
+(* s ; u |= s->Prop *)
+
+Program Definition bool_to_Prop'@{s;u} (b : bool@{s;u}) : Prop := _.
+Next Obligation.
+  intro b; destruct b.
+  - exact True.
+  - exact False.
+Defined.
+(* s ; u |= s->Type *)
+
+Inductive unit@{s;u} : Type@{s;u} := tt.
+
+#[universes(polymorphic=no)]
+Sort Test.
+Check (match true@{Test;Set} return ?[P] with true => tt | false => tt end).
diff --git a/test-suite/success/sort_poly_elim_csts.v b/test-suite/success/sort_poly_elim_csts.v
index fa8e1e5af325..8d5783a8e690 100644
--- a/test-suite/success/sort_poly_elim_csts.v
+++ b/test-suite/success/sort_poly_elim_csts.v
@@ -73,28 +73,28 @@ Definition sumor_sind := sum_elim@{Type Prop Type SProp;_ _ _}.
 Definition sumor_rect := sum_elim@{Type Prop Type Type;_ _ _}.
 Definition sumor_ind := sum_elim@{Type Prop Type Prop;_ _ _}.
 
-Fail Definition idT@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+Fail Definition idT@{sl sr s;ul ur|} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
   : sum@{sl sr Type;ul ur} A B :=
   match x return sum@{sl sr Type;ul ur} A B with
   | inl a => inl a
   | inr b => inr b
   end.
 
-Fail Definition idP@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+Fail Definition idP@{sl sr s;ul ur|} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
   : sum@{sl sr Prop;ul ur} A B :=
   match x return sum@{sl sr Prop;ul ur} A B with
   | inl a => inl a
   | inr b => inr b
   end.
 
-Fail Definition idS@{sl sr s;ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+Fail Definition idS@{sl sr s;ul ur|} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
   : sum@{sl sr SProp;ul ur} A B :=
   match x return sum@{sl sr SProp;ul ur} A B with
   | inl a => inl a
   | inr b => inr b
   end.
 
-Fail Definition idV@{sl sr s s';ul ur} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
+Fail Definition idV@{sl sr s s';ul ur|} (A : Type@{sl;ul}) (B : Type@{sr;ur}) (x : sum@{sl sr s;ul ur} A B)
   : sum@{sl sr s';ul ur} A B :=
   match x return sum@{sl sr s';ul ur} A B with
   | inl a => inl a
@@ -145,19 +145,19 @@ Definition list'_elim@{s s0 s';l l'|s0 -> s'}
     | cons' x l => fc x l (F l)
     end.
 
-Fail Fixpoint list'_idT@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Type;l} A :=
+Fail Fixpoint list'_idT@{s s';l|} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Type;l} A :=
   match l with
   | nil' => nil'
   | cons' x l => cons' x (list'_idT l)
   end.
 
-Fail Fixpoint list'_idP@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Prop;l} A :=
+Fail Fixpoint list'_idP@{s s';l|} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s Prop;l} A :=
   match l with
   | nil' => nil'
   | cons' x l => cons' x (list'_idP l)
   end.
 
-Fail Fixpoint list'_idS@{s s';l} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s SProp;l} A :=
+Fail Fixpoint list'_idS@{s s';l|} {A : Type@{s;l}} (l : List'@{s s';l} A) : List'@{s SProp;l} A :=
   match l with
   | nil' => nil'
   | cons' x l => cons' x (list'_idS l)