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 /parsing/extend.ml | |
| parent | 306f862507c278f6865b82e5443f9d47742b2bc5 (diff) | |
[pcoq] Remove unneeded casting operators.
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 8dc77e1216..ed6ebe5aed 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -81,8 +81,8 @@ type ('a,'b,'c) ty_user_symbol = (* Should be merged with gramlib's implementation *) -type norec = NoRec (* just two *) -type mayrec = MayRec (* incompatible types *) +type norec = Gramlib.Grammar.ty_norec +type mayrec = Gramlib.Grammar.ty_mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol |