Merge PR #6197: [plugin] Remove LocalityFixme über hack.

7 files changed, 25 insertions, 40 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/vernacentries.ml b/vernac/vernacentries.ml
index 6191f3708..62c7edb19 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2078,7 +2078,7 @@ let interp ?proof ?loc locality poly st c =
   (* Extensions *)
   | VernacExtend (opn,args) ->
     (* XXX: Here we are returning the state! :) *)
-    let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in
+    let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in
     ()
 
 (* Vernaculars that take a locality flag *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1d024386e..47dec1958 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -11,8 +11,16 @@ open Pp
 open CErrors
 
 type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
-  Vernacstate.t -> Vernacstate.t
+
+type atts = {
+  loc : Loc.t option;
+  locality : bool option;
+}
+
+type vernac_command =
+  Genarg.raw_generic_argument list ->
+  atts:atts -> st:Vernacstate.t ->
+  Vernacstate.t
 
 (* Table of vernac entries *)
 let vernac_tab =
@@ -66,10 +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 res = hunk loc in
-    Locality.LocalityFixme.assert_consumed ();
-    res
+    let atts = { loc; locality } in
+    hunk ~atts
   with
     | Drop -> raise Drop
     | reraise ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 1c66b1c04..602ccba15 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,8 +10,15 @@
 
 type deprecation = bool
 
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
-  Vernacstate.t -> Vernacstate.t
+type atts = {
+  loc : Loc.t option;
+  locality : bool option;
+}
+
+type vernac_command =
+  Genarg.raw_generic_argument list ->
+  atts:atts -> st:Vernacstate.t ->
+  Vernacstate.t
 
 val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
 
@@ -21,4 +28,4 @@ val vinterp_init : unit -> unit
 
 val call : ?locality:bool -> ?loc:Loc.t ->
   Vernacexpr.extend_name * Genarg.raw_generic_argument list ->
-  Vernacstate.t -> Vernacstate.t
+  st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 9802a03ca..eb1359d52 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type t = { (* TODO: inline records in OCaml 4.03 *)
+type t = {
   system  : States.state;        (* summary + libstack *)
   proof   : Proof_global.state;  (* proof state *)
   shallow : bool                 (* is the state trimmed down (libstack) *)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 63a5b3b1e..bcfa49aa3 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type t = { (* TODO: inline records in OCaml 4.03 *)
+type t = {
   system  : States.state;        (* summary + libstack *)
   proof   : Proof_global.state;  (* proof state *)
   shallow : bool                 (* is the state trimmed down (libstack) *)