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

1 files changed, 8 insertions, 4 deletions

diff --git a/API/API.mli b/API/API.mli
index 67e73dfdf8..1f1b05eadb 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5966,9 +5966,6 @@ end
 module Locality :
 sig
   val make_section_locality : bool option -> bool
-  module LocalityFixme : sig
-    val consume : unit -> bool option
-  end
   val make_module_locality : bool option -> bool
 end
 
@@ -6111,8 +6108,15 @@ sig
 
   type deprecation = bool
 
+  type atts = {
+    loc : Loc.t option;
+    locality : bool option;
+  }
+
   type vernac_command =
-    Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t
+    Genarg.raw_generic_argument list ->
+    atts:atts -> st:Vernacstate.t ->
+    Vernacstate.t
 
   val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit