diff options
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 3790f36e5a..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -195,7 +195,7 @@ Cumulative, NonCumulative This means that two instances of the same inductive type (family) are convertible only if all the universes are equal. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + .. exn:: The cumulative attribute can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, i.e. either having the :flag:`Universe Polymorphism` flag on, or diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2edd9d4d11..0f63dfe5ce 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -674,7 +674,7 @@ let is_polymorphic_inductive_cumulativity = let polymorphic_cumulative = let error_poly_context () = user_err - Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + Pp.(str "The cumulative attribute can only be used in a polymorphic context."); in let open Attributes in let open Notations in |