Fix refman

Author: mattam82

doc/sphinx/addendum/universe-polymorphism.rst

@@ -538,6 +538,10 @@ Explicit Universes
    | Type
    | _
    | @qualid
+   sort_quality_var ::= Prop
+      | SProp
+      | Type
+      | @qualid
    sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
    cumul_sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* {? {| + | = | * } } @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
    sort_poly_constraint ::= @universe_name {| < | = | <= } @universe_name
@@ -810,7 +814,7 @@ All sort quality variables must be explicitly bound.
 
       Polymorphic Definition sort'@{s | u |} := Type@{s|u}.
 
-   To help the parser, both `|` in the :n:`@univ_decl` are required.
+   To help the parser, both `|` in the :n:`@sort_poly_decl` are required.
 
 Sort quality variables of a sort polymorphic definition may be
 instantiated by the concrete values `SProp`, `Prop` and `Type` or by a