diff options
Diffstat (limited to 'doc/sphinx/addendum/universe-polymorphism.rst')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 41afe3c312..99b883d23c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -386,8 +386,10 @@ to universes and explicitly instantiate polymorphic definitions. global constraint on polymorphic universes. .. exn:: Undeclared universe @ident. + :undocumented: .. exn:: Universe inconsistency. + :undocumented: Polymorphic definitions |