diff options
| author | Pierre-Marie Pédrot | 2020-03-08 00:30:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 00:30:20 +0100 |
| commit | 83d15b4d686349da0fbd46ea080ee45368d6a964 (patch) | |
| tree | 1066cc5145193e228cbd9cee6d2f3cbf29e8302c /parsing/extend.ml | |
| parent | 47a65ee1db1ea8320e27da880f53cfa87d8e0f99 (diff) | |
| parent | b095fc74b7f0be690a5313b992d4d4750c86875f (diff) | |
Merge PR #11714: [gramlib] Refactor gramlib interface.
Reviewed-by: ppedrot
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 |