From b402adc12c00ba72046423d3a1737ccad517f70e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 11 Oct 2020 18:39:16 -0700
Subject: Rename operconstr -> term

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 0c51361b64..94a705a4c6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -510,7 +510,7 @@ Displaying information about notations
 
    The output for `Print Grammar constr` includes :cmd:`Notation` definitions,
    which are dynamically added to the grammar at run time.
-   For example, in the definition for `operconstr`, the production on the second line shown
+   For example, in the definition for `term`, the production on the second line shown
    here is defined by a :cmd:`Reserved Notation` command in `Notations.v`::
 
      | "50" LEFTA
-- 
cgit v1.2.3


From ede77b72328c98995c0636656bb71ba87861ddfe Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 11 Oct 2020 19:15:51 -0700
Subject: Rename tactic_expr -> ltac_expr

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 94a705a4c6..fc5aa3f93d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -477,10 +477,10 @@ Displaying information about notations
    such as `1+2*3` in the usual way as `1+(2*3)`.  However, most nonterminals have a single level.
 
    For example, this output from `Print Grammar tactic` shows the first 3 levels for
-   `tactic_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
+   `ltac_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
    which applies to the productions within it, such as the `try` construct::
 
-     Entry tactic_expr is
+     Entry ltac_expr is
      [ "5" RIGHTA
        [ binder_tactic ]
      | "4" LEFTA
-- 
cgit v1.2.3


From 41b07808c84a86ea4b77e0c7855b22bfd3906669 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 12 Oct 2020 21:55:00 -0700
Subject: Rename misc nonterminals

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fc5aa3f93d..06018304ab 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -444,7 +444,7 @@ Displaying information about notations
 
    This command doesn't display all nonterminals of the grammar.  For example,
    productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
-   and `tactic_then_gen` which are not shown and can't be printed.
+   and `for_each_goal` which are not shown and can't be printed.
 
    Most of the grammar in the documentation was updated in 8.12 to make it accurate and
    readable.  This was done using a new developer tool that extracts the grammar from the
@@ -486,7 +486,7 @@ Displaying information about notations
      | "4" LEFTA
        [ SELF; ";"; binder_tactic
        | SELF; ";"; SELF
-       | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
+       | SELF; ";"; tactic_then_locality; for_each_goal; "]" ]
      | "3" RIGHTA
        [ IDENT "try"; SELF
        :
-- 
cgit v1.2.3