diff options
| author | Emilio Jesus Gallego Arias | 2020-02-28 16:06:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-28 16:06:23 -0500 |
| commit | b095fc74b7f0be690a5313b992d4d4750c86875f (patch) | |
| tree | 8b4c5f5fb09e0ac6ba48ac2a9523259df83f9c33 /parsing/extend.ml | |
| parent | 5c7d89641085e125471db089239e73a064073024 (diff) | |
[gramlib] Refactor gramlib interface.
This is in preparation for making the Gramlib interface the canonical
one; see #11647 .
I tried to implement some of the ideas that were floated around in a
chat with Pierre-Marie, suggestions / comments are welcome.
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 |