Skip to content

Commit

Permalink
try to shorten modules table
Browse files Browse the repository at this point in the history
  • Loading branch information
Villetaneuse committed Aug 1, 2024
1 parent 9710d79 commit 440bb6b
Showing 1 changed file with 15 additions and 5 deletions.
20 changes: 15 additions & 5 deletions doc/sphinx/language/core/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand All @@ -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`
Expand Down Expand Up @@ -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`
Expand Down

0 comments on commit 440bb6b

Please sign in to comment.