From af7628468d638c77fb3f55a9eb315b687b76a21d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 12:20:00 -0500
Subject: [parsing] Remove redundant interfaces from Pcoq

There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.

A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
---
 vernac/egramcoq.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/egramcoq.ml')

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 88bcf1d477..7a52f53dc0 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -332,8 +332,8 @@ let make_sep_rules = function
     Pcoq.G.Symbol.rules ~warning:None [r]
 
 type ('s, 'a) mayrec_symbol =
-| MayRecNo : ('s, norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
-| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
   if is_binder_level custom from p
@@ -458,8 +458,8 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
     ty_eval rem f { env with constrs; constrlists; }
 
 type ('s, 'a, 'r) mayrec_rule =
-| MayRecRNo : ('s, norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
 
 let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
 | TyStop -> MayRecRNo G.Rule.stop
-- 
cgit v1.2.3