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/proof-engine/ltac.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 5c091f04ac..8663ac646b 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -161,7 +161,7 @@ Syntactic values
 Provides a way to use the syntax and semantics of a grammar nonterminal as a
 value in an :token:`ltac_expr`.  The table below describes the most useful of
 these.  You can see the others by running ":cmd:`Print Grammar` `tactic`" and
-examining the part at the end under "Entry tactic:tactic_arg".
+examining the part at the end under "Entry tactic:tactic_value".
 
    :token:`ident`
       name of a grammar nonterminal listed in the table
-- 
cgit v1.2.3


From 480d34fc22c195d4b19f639345fa993652838894 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 22 Oct 2020 21:32:48 -0700
Subject: Change a few nonterminal names in mlgs and update doc to match

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 770de9a6c3..cdbae8ade1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5724,11 +5724,11 @@ respectively.
 
    local function definition
 
-.. tacv:: pose fix @fix_body
+.. tacv:: pose fix @fix_decl
 
    local fix definition
 
-.. tacv:: pose cofix @fix_body
+.. tacv:: pose cofix @fix_decl
 
    local cofix definition
 
-- 
cgit v1.2.3