aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-24 20:30:49 +0100
committerEmilio Jesus Gallego Arias2018-11-27 15:12:04 +0100
commit786a522c18aa39a6d1d8312bd70132dfbfd16df6 (patch)
treefc7655f4e6cbba12af6f57103543b903e736637a /parsing/pcoq.mli
parent1655407ac0525efa0fcd98ab85e3fd80a9f6cf64 (diff)
[pcoq] Remove a redundant `entry` type.
This was done in a bit of redundant way when we removed the camlp4 compat layer; we fix this and make the type flow clearer.
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a5b83d193d..69ba57d516 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -26,7 +26,7 @@ sig
end
module Entry : sig
- type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+ type 'a t = 'a Extend.entry
val create : string -> 'a t
val parse : 'a t -> Parsable.t -> 'a
val print : Format.formatter -> 'a t -> unit