diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 06cd69c167869..86cbf827e1560 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -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