From 062067f8878b82d44ddcb5269bb4b4588262397f Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Thu, 4 Jul 2024 18:12:20 +0200
Subject: [PATCH] Hint is not a command

---
 doc/sphinx/language/core/modules.rst | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 1cd13a970d7e6..5886b2b28f057 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -1071,8 +1071,10 @@ outside the module.
   :header-rows: 1
 
   * - ``Command``
-    - without attribute, not imported
-    - without attribute, imported
+    - without attribute,
+      not imported
+    - without attribute,
+      imported
     - :attr:`local`
     - :attr:`export`
     - :attr:`global`
@@ -1098,7 +1100,7 @@ outside the module.
     - attribute not supported
     - same as without attribute
 
-  * - :cmd:`Hint` (and :cmd:`Instance`)
+  * - ``Hints`` (and :cmd:`Instance`)
     - not available outside
     - available outside
     - not available outside