diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 02:59:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-19 02:59:42 +0200 |
| commit | a2b23ba26066944685e6c5a58e8cfc87c3aa9a2c (patch) | |
| tree | ef07207d4b5aa870cf6a9ed4e833e7fda6d57af0 /gramlib/grammar.mli | |
| parent | 306f862507c278f6865b82e5443f9d47742b2bc5 (diff) | |
[pcoq] Remove unneeded casting operators.
Diffstat (limited to 'gramlib/grammar.mli')
| -rw-r--r-- | gramlib/grammar.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 658baf1de9..9e48460206 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -19,6 +19,9 @@ module type GLexerType = Plexing.Lexer (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -36,8 +39,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules |