aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index dad98e2e9..3f014c4c8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -171,7 +171,6 @@ module Symbols : sig
val sopt : G.symbol -> G.symbol
val snterml : G.internal_entry * string -> G.symbol
val snterm : G.internal_entry -> G.symbol
- val snterml_level : G.symbol -> string
end = struct
let stoken tok =
@@ -199,10 +198,6 @@ end = struct
let slist1 x = Gramext.Slist1 x
let sopt x = Gramext.Sopt x
- let snterml_level = function
- | Gramext.Snterml (_, l) -> l
- | _ -> failwith "snterml_level"
-
end
let camlp4_verbosity silent f x =
@@ -211,8 +206,6 @@ let camlp4_verbosity silent f x =
f x;
warning_verbose := a
-let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x
-
(** Grammar extensions *)
(** NB: [extend_statment =