diff options
| -rw-r--r-- | parsing/extend.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
3 files changed, 2 insertions, 4 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 = 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) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f83109d39a..e12a1cc11b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -24,7 +24,7 @@ sig end module Entry : sig - type 'a t = 'a Extend.entry + type 'a t val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit |