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/egramml.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/egramml.ml')
| -rw-r--r-- | vernac/egramml.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 00a239f56e..981de78162 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -24,9 +24,9 @@ type 's grammar_prod_item = type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = -| TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.G.Symbol.t * 'b ty_arg option -> - ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule +| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.Symbol.t * 'b ty_arg option -> + ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule |