diff options
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 848861238a..c53c3f02a8 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -10,7 +10,7 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.e +type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.t type side = Left | Right @@ -82,8 +82,8 @@ type ('a,'b,'c) ty_user_symbol = (* Should be merged with gramlib's implementation *) -type norec = Gramlib.Grammar.ty_norec -type mayrec = Gramlib.Grammar.ty_mayrec +type norec = Gramlib.Grammar.norec +type mayrec = Gramlib.Grammar.mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol |