diff options
| author | Emilio Jesus Gallego Arias | 2020-02-20 22:51:46 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | f9174f64c56375adb42e53b97df9eeb8b0a9680d (patch) | |
| tree | 95cf27fd7d8afd694d89d8f0f3bbb65811892f41 /parsing/extend.ml | |
| parent | d5dcb490f4f08dc1f5ae4158a26d264e03f808cc (diff) | |
[parsing] Remove unneeded `Extend.entry` type.
This is not needed anymore after the unification.
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 9c7f5c87c4..fadfb6c5f4 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -10,8 +10,6 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.t - type side = Left | Right type production_position = |