From f5952c10856791b10393c0bfb9dc55277d41a5c7 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sun, 15 Dec 2019 04:52:13 +0900 Subject: Extend `Print Canonical Projections` with a search functionality The `Print Canonical Projections` command now can take constants and prints only the unification rules that involves or are synthesized from given constants. --- .../10747-canonical-better-message.rst | 5 +++++ doc/sphinx/language/gallina-extensions.rst | 15 +++++++++++---- 2 files changed, 16 insertions(+), 4 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/10747-canonical-better-message.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst new file mode 100644 index 0000000000..e73be9c642 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst @@ -0,0 +1,5 @@ +- **Changed:** + The :cmd:`Print Canonical Projections` command now can take constants and + prints only the unification rules that involve or are synthesized from given + constants (`#10747 `_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8caa289a47..4ca20ce313 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2075,11 +2075,13 @@ in :ref:`canonicalstructures`; here only a simple example is given. This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. -.. cmd:: Print Canonical Projections +.. cmd:: Print Canonical Projections {* @ident} This displays the list of global names that are components of some canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. + which it is a projection is indicated. If constants are given as + its arguments, only the unification rules that involve or are + synthesized from given constants will be shown. .. example:: @@ -2089,10 +2091,15 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. coqtop:: all + + Print Canonical Projections nat. + .. note:: - The last line would not show up if the corresponding projection (namely - :g:`Prf_equiv`) were annotated as not canonical, as described above. + The last line in the first example would not show up if the + corresponding projection (namely :g:`Prf_equiv`) were annotated as not + canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 471400e724317963983a0670a4c3437b1dcc61d5 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 28 Dec 2019 01:56:05 +0900 Subject: Update doc/sphinx/language/gallina-extensions.rst Co-Authored-By: Cyril Cohen --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 4ca20ce313..a8d6d2632b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2081,7 +2081,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. canonical structure. For each of them, the canonical structure of which it is a projection is indicated. If constants are given as its arguments, only the unification rules that involve or are - synthesized from given constants will be shown. + synthesized from simultaneously all given constants will be shown. .. example:: -- cgit v1.2.3