doc for Ltac2 Globalize/Check

SkySkimmer · Oct 11, 2023 · 4bb109d · 4bb109d
1 parent 8d460e9
commit 4bb109d
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 2 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18139-ltac2printers.rst b/doc/changelog/06-Ltac2-language/18139-ltac2printers.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  :cmd:`Ltac2 Globalize` and :cmd:`Ltac2 Check` useful to investigate the expansion of Ltac2 notations
+  (`#18139 <https://github.com/coq/coq/pull/18139>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
@@ -350,6 +350,14 @@ Printing Ltac2 tactics
    :cmd:`Print` can print defined Ltac2 tactics and can avoid printing
    other objects by using `Print Ltac2`.
 
+.. cmd:: Ltac2 Globalize @ltac2_expr
+
+   Prints the result of resolving notations in the given expression.
+
+.. cmd:: Ltac2 Check @ltac2_expr
+
+   Typechecks the given expression and prints the result.
+
 .. cmd:: Print Ltac2 Signatures
 
    This command displays a list of all defined tactics in scope with their types.

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -434,10 +434,11 @@ Requests to the environment
 
 .. cmd:: Locate Ltac @qualid
 
-   Like :cmd:`Locate`, but limits the search to tactics
+   Like :cmd:`Locate`, but limits the search to Ltac tactics
 
 .. cmd:: Locate Ltac2 @qualid
-   :undocumented:
+
+   Like :cmd:`Locate`, but limits the search to Ltac2 tactics.
 
 .. cmd:: Locate Library @qualid
 

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -692,6 +692,8 @@ command: [
 | "Print" "Ltac2" reference      (* ltac2 plugin *)
 | "Locate" "Ltac2" reference      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
+| "Ltac2" "Check" ltac2_expr6      (* ltac2 plugin *)
+| "Ltac2" "Globalize" ltac2_expr6      (* ltac2 plugin *)
 ]
 
 reference_or_constr: [

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -960,6 +960,8 @@ command: [
 | "Print" "Ltac2" qualid      (* ltac2 plugin *)
 | "Locate" "Ltac2" qualid      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
+| "Ltac2" "Check" ltac2_expr      (* ltac2 plugin *)
+| "Ltac2" "Globalize" ltac2_expr      (* ltac2 plugin *)
 | "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident )
 | "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident )
 | "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident )