From 4bb109d3051f111cc67f3cdd827817f1f1b4e7af Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 9 Oct 2023 16:31:49 +0200 Subject: [PATCH] doc for Ltac2 Globalize/Check --- doc/changelog/06-Ltac2-language/18139-ltac2printers.rst | 4 ++++ doc/sphinx/proof-engine/ltac2.rst | 8 ++++++++ doc/sphinx/proof-engine/vernacular-commands.rst | 5 +++-- doc/tools/docgram/fullGrammar | 2 ++ doc/tools/docgram/orderedGrammar | 2 ++ 5 files changed, 19 insertions(+), 2 deletions(-) create mode 100644 doc/changelog/06-Ltac2-language/18139-ltac2printers.rst diff --git a/doc/changelog/06-Ltac2-language/18139-ltac2printers.rst b/doc/changelog/06-Ltac2-language/18139-ltac2printers.rst new file mode 100644 index 0000000000000..f1ed57669610d --- /dev/null +++ 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 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index ea9a6c998c114..8cb9384c2c486 100644 --- 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 index 1a7baf4aba14e..4d6cb6c8f40ca 100644 --- 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 index 504495b7b8637..ea8b73fd39688 100644 --- 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 index b48fccf2a518a..7b7a1429c4aaa 100644 --- 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 )