Fix About info about squashing

The previous version is incorrect (it assumes the order is just Prop <= Type with SProp unrelated)

test-suite/output/Inductive.out

@@ -50,7 +50,7 @@ sempty is universe polymorphic
 sempty@{q | } may only be eliminated to produce values whose type is in sort quality q,
   unless instantiated such that the quality SProp
   is equal to the instantiation of q,
-  or to Prop or Type if q is instantiated to Type.
+  or to constant qualities smaller (SProp <= Prop <= Type) than the instantiation of q.
 Expands to: Inductive Inductive.sempty
 ssig@{q1 q2 q3 | a b} :
 forall A : Type@{q1 | a}, (A -> Type@{q2 | b}) -> Type@{q3 | max(a,b)}
@@ -60,7 +60,7 @@ ssig is universe polymorphic
 ssig@{q1 q2 q3 | a b} may only be eliminated to produce values whose type is in sort quality q3,
   unless instantiated such that the qualities q1, q2 and Prop
   are equal to the instantiation of q3,
-  or to Prop or Type if q3 is instantiated to Type.
+  or to constant qualities smaller (SProp <= Prop <= Type) than the instantiation of q3.
 Arguments ssig A%type_scope B%function_scope
 Expands to: Inductive Inductive.ssig
 BoxP@{q | a} : Type@{q | a} -> Prop

vernac/prettyp.ml

@@ -240,7 +240,7 @@ let print_squash env ref udecl = match ref with
             | QSort (q,_) ->
               let ppq = Termops.pr_evd_qvar sigma q in
               str "equal to the instantiation of " ++ ppq ++ pr_comma() ++
-              str "or to Prop or Type if " ++ ppq ++ str " is instantiated to Type"
+              str "or to constant qualities smaller (SProp <= Prop <= Type) than the instantiation of " ++ ppq
           in
           let qs = Sorts.Quality.Set.elements qs in
           let quality_s, is_s = match qs with