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

---
 plugins/ltac/pltac.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac/pltac.ml')

diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index b7b54143df..1631215d58 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -38,7 +38,8 @@ let clause_dft_concl =
 
 (* Main entries for ltac *)
 let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+let ltac_expr = Entry.create "ltac_expr"
+let tactic_expr = ltac_expr
 let binder_tactic = Entry.create "binder_tactic"
 
 let tactic = Entry.create "tactic"
-- 
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

---
 plugins/ltac/pltac.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac/pltac.ml')

diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1631215d58..94e398fe5d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -37,7 +37,8 @@ let clause_dft_concl =
 
 
 (* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic_arg"
+let tactic_value = Entry.create "tactic_value"
+let tactic_arg = tactic_value
 let ltac_expr = Entry.create "ltac_expr"
 let tactic_expr = ltac_expr
 let binder_tactic = Entry.create "binder_tactic"
-- 
cgit v1.2.3