diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.mli | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e12ccaa636..c21f8f0d9a 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -26,14 +26,10 @@ module Gram : sig type 'a entry = 'a Entry.e [@@ocaml.deprecated "Use [Pcoq.Entry.t]"] - [@@@ocaml.warning "-3"] - - val entry_create : string -> 'a entry + val entry_create : string -> 'a Entry.e [@@ocaml.deprecated "Use [Pcoq.Entry.create]"] - val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit - - [@@@ocaml.warning "+3"] + val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e |
