From ce418aea93a6396412de57aded0ff092bec7596b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 12:26:59 +0100
Subject: [plugin] Encapsulate modifiers to vernac commands.

This is a continuation on #6183 and another step towards a more
functional interpretation of commands.

In particular, this should allow us to remove the locality hack.
---
 API/API.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 86c6f14158..f56509a70a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5982,8 +5982,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
 
-- 
cgit v1.2.3


From 57f62f06419972ba799e451d2f56552dc1b2fb63 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 15:42:18 +0100
Subject: [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.
---
 API/API.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index f56509a70a..275185fa7d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5837,9 +5837,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
 
-- 
cgit v1.2.3