3 files changed, 1 insertions, 32 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
diff --git a/vernac/locality.mli b/vernac/locality.mli
index c1c45d6b0..bef66d8bc 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -41,11 +41,3 @@ val enforce_section_locality : bool option -> bool -> bool
 
 val make_module_locality : bool option -> bool
 val enforce_module_locality : bool option -> bool -> bool
-
-(* This is the old imperative interface that is still used for
- * VernacExtend vernaculars.  Time permitting this could be trashed too *)
-module LocalityFixme : sig
-  val set : bool option -> unit
-  val consume : unit -> bool option
-  val assert_consumed : unit -> unit
-end
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 725436fef..47dec1958 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -74,11 +74,8 @@ let call ?locality ?loc (opn,converted_args) =
     phase := "Checking arguments";
     let hunk = callback converted_args in
     phase := "Executing command";
-    Locality.LocalityFixme.set locality;
     let atts = { loc; locality } in
-    let res = hunk ~atts in
-    Locality.LocalityFixme.assert_consumed ();
-    res
+    hunk ~atts
   with
     | Drop -> raise Drop
     | reraise ->