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.ml | |
| parent | 306f862507c278f6865b82e5443f9d47742b2bc5 (diff) | |
[pcoq] Remove unneeded casting operators.
Diffstat (limited to 'gramlib/grammar.ml')
| -rw-r--r-- | gramlib/grammar.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index f86cb0f6f2..ff0b90dcff 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -10,6 +10,9 @@ open Util module type GLexerType = Plexing.Lexer +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -27,8 +30,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 @@ -92,9 +93,6 @@ let tokens con = egram.gtokens; !list -type ty_norec = TyNoRec -type ty_mayrec = TyMayRec - type ('a, 'b, 'c) ty_and_rec = | NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec | MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec |