aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/pcoq.mli8
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