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

---
 dev/doc/parsing.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev/doc')

diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md
index 4982e3e94d..4956b91d01 100644
--- a/dev/doc/parsing.md
+++ b/dev/doc/parsing.md
@@ -210,7 +210,7 @@ command.  The first square bracket around a nonterminal definition is for groupi
 level definitions, which are separated with `|`, for example:
 
   ```
-  tactic_expr:
+  ltac_expr:
       [ "5" RIGHTA
         [ te = binder_tactic -> { te } ]
       | "4" LEFTA
@@ -220,8 +220,8 @@ level definitions, which are separated with `|`, for example:
 Grammar extensions can specify what level they are modifying, for example:
 
   ```
-  tactic_expr: LEVEL "1" [ RIGHTA
-    [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+  ltac_expr: LEVEL "1" [ RIGHTA
+    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
     ] ];
   ```
 
-- 
cgit v1.2.3