From 767ecfec49543b70a605d20b1dae8252e1faabfe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 19 Aug 2019 03:17:25 +0200
Subject: [parsing] Make grammar rules private.

After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
---
 plugins/ltac/tacentries.ml | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 53b5386375..6b83590b1d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -406,15 +406,21 @@ let create_ltac_quotation name cast (e, l) =
   let level = None in
   let assoc = None in
   let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Pcoq.G.Symbol.token (CLexer.terminal name)),
-      Pcoq.G.Symbol.token (CLexer.terminal ":")),
-      Pcoq.G.Symbol.token (CLexer.terminal "(")),
-      entry),
-      Pcoq.G.Symbol.token (CLexer.terminal ")"))
+    Pcoq.G.(
+      Rule.next
+        (Rule.next
+           (Rule.next
+              (Rule.next
+                 (Rule.next
+                    Rule.stop
+                    (Symbol.token (CLexer.terminal name)))
+                 (Symbol.token (CLexer.terminal ":")))
+              (Symbol.token (CLexer.terminal "(")))
+           entry)
+        (Symbol.token (CLexer.terminal ")")))
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
+  let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
   Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
 
 (** Command *)
-- 
cgit v1.2.3