aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cdf72bb1e..224d9765f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -372,9 +372,6 @@ let locality_flag = ref None
let local_of_bool = function true -> Local | false -> Global
-let is_true = function Some (_,b) -> b | _ -> false
-let is_false = function Some (_,b) -> not b | _ -> false
-
let check_locality () =
match !locality_flag with
| Some (loc,true) ->