[plugin] Remove LocalityFixme über hack.

To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.

This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.

3 files changed, 1 insertions, 32 deletions

diff --git a/vernac/locality.ml b/vernac/locality.ml
index 054a451a46..681b1ab207 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 c1c45d6b0f..bef66d8bc5 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 725436fefa..47dec19588 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 ->