aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-20 22:51:46 -0500
committerEmilio Jesus Gallego Arias2020-03-25 23:45:00 -0400
commitf9174f64c56375adb42e53b97df9eeb8b0a9680d (patch)
tree95cf27fd7d8afd694d89d8f0f3bbb65811892f41 /parsing/pcoq.ml
parentd5dcb490f4f08dc1f5ae4158a26d264e03f808cc (diff)
[parsing] Remove unneeded `Extend.entry` type.
This is not needed anymore after the unification.
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index e10e4bb8dd..7d301e75bd 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -29,7 +29,7 @@ module G : sig
val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
val mk_rule : 'a Tok.p list -> string Rules.t
-end with type 'a Entry.t = 'a Extend.entry = struct
+end = struct
module G_ = Grammar.GMake(CLexer.Lexer)