Skip to content

Commit

Permalink
Update doc/sphinx/language/core/modules.rst
Browse files Browse the repository at this point in the history
Co-authored-by: Gaëtan Gilbert <[email protected]>
  • Loading branch information
Villetaneuse and SkySkimmer authored Jul 4, 2024
1 parent 5b0a29d commit 3b7fb67
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/sphinx/language/core/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -1119,7 +1119,7 @@ outside the module.
- attribute not supported
- same as without attribute

* - :cmd:`Tactic`
* - :cmd:`Ltac`
- available with qualified name
- available with short name
- not available outside
Expand Down

0 comments on commit 3b7fb67

Please sign in to comment.