diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 4c2ca4b25262..edca38a58aec 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -699,11 +699,15 @@ A similar table for :cmd:`Section` can be found - :attr:`export` - :attr:`global` - * - :cmd:`Definition`, :cmd:`Lemma`, :cmd:`Axiom`, ... + * - :cmd:`Definition`, :cmd:`Lemma`, + + :cmd:`Axiom`, ... - :attr:`global` - qualified name - ❌ - - short name when imported + - short name + + when imported * - :cmd:`Notation` - :attr:`global` @@ -715,7 +719,9 @@ A similar table for :cmd:`Section` can be found - :attr:`global` - not available - ❌ - - short name when imported + - short name + + when imported * - ``Hints`` (and :cmd:`Instance`) - :attr:`export` @@ -747,13 +753,17 @@ A similar table for :cmd:`Section` can be found - :attr:`global` - not available - ❌ - - short name when imported + - short name + + when imported * - :cmd:`Ltac2` - :attr:`global` - not available - ❌ - - short name when imported + - short name + + when imported * - :cmd:`Tactic Notation` - :attr:`global`