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