aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-02 16:04:50 +0200
committerMaxime Dénès2017-05-02 16:04:50 +0200
commit28accc370aa2f6fafbf50b69be7ae5dc06104212 (patch)
tree7764de5a598390e9906f064170a480cfcfe0a38d /parsing/pcoq.ml
parent63503b99c46b27009e85e5c0fa9588b7424a589d (diff)
parent9a48211ea8439a8502145e508b70ede9b5929b2f (diff)
Merge PR#582: Fix warnings
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml8
1 files changed, 0 insertions, 8 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index dad98e2e98..9a4766c0bf 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open CErrors
open Util
open Extend
@@ -171,7 +170,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 +197,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 +205,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 =