diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 12:20:00 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | af7628468d638c77fb3f55a9eb315b687b76a21d (patch) | |
| tree | 63cfb1a71815b956d5a79cf83b4d5284626d1d1e /vernac/egramcoq.ml | |
| parent | f9174f64c56375adb42e53b97df9eeb8b0a9680d (diff) | |
[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.
Diffstat (limited to 'vernac/egramcoq.ml')
| -rw-r--r-- | vernac/egramcoq.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |