aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 20:04:58 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:39:25 +0200
commit02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch)
tree5e55f22c5b20dcf694c00741a69dae6f1d993267 /parsing/pcoq.ml
parent95239fa33c5da60080833dabc3ced246680dfdf9 (diff)
Remove some unused values and types
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 =