aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/locality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/locality.ml')
-rw-r--r--vernac/locality.ml20
1 files changed, 0 insertions, 20 deletions
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 054a451a4..681b1ab20 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -6,22 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-
(** * Managing locality *)
let local_of_bool = function
| true -> Decl_kinds.Local
| false -> Decl_kinds.Global
-let check_locality locality_flag =
- match locality_flag with
- | Some b ->
- let s = if b then "Local" else "Global" in
- CErrors.user_err ~hdr:"Locality.check_locality"
- (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
- | None -> ()
-
(** Extracting the locality flag *)
(* Commands which supported an inlined Local flag *)
@@ -95,13 +85,3 @@ let make_module_locality = function
let enforce_module_locality locality_flag local =
make_module_locality (enforce_locality_full locality_flag local)
-
-module LocalityFixme = struct
- let locality = ref None
- let set l = locality := l
- let consume () =
- let l = !locality in
- locality := None;
- l
- let assert_consumed () = check_locality !locality
-end