diff options
| author | Emilio Jesus Gallego Arias | 2018-11-24 20:30:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-27 15:12:04 +0100 |
| commit | 786a522c18aa39a6d1d8312bd70132dfbfd16df6 (patch) | |
| tree | fc7655f4e6cbba12af6f57103543b903e736637a /parsing/pcoq.mli | |
| parent | 1655407ac0525efa0fcd98ab85e3fd80a9f6cf64 (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.mli | 2 |
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 |
