From 4aba7c162905c61b3bb1a9f8d5c325de38b5847a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 16:19:41 +0100
Subject: [vernac] Start to uniformize type of vernac interpretation.

In particular, we put all the context in the atts structure, and
generalize the type of the parameters of a vernac.

I hope this helps people working on "attributes", my motivation is
indeed having a more robust interpretation.
---
 API/API.mli | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 7ec3cbee3b..85cd644b09 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6114,12 +6114,11 @@ sig
     locality : bool option;
   }
 
-  type vernac_command =
-    Genarg.raw_generic_argument list ->
-    atts:atts -> st:Vernacstate.t ->
-    Vernacstate.t
+  type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
-  val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
+  type plugin_args = Genarg.raw_generic_argument list
+
+  val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
 end
 
-- 
cgit v1.2.3


From 6f240e9b15f2b6f6622c811933c4f5ffdf78cceb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 16:28:02 +0100
Subject: [vernac] Add polymorphic to the type of vernac interpration options.

---
 API/API.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 85cd644b09..ec6a68ebb0 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6112,6 +6112,7 @@ sig
   type atts = {
     loc : Loc.t option;
     locality : bool option;
+    polymorphic : bool;
   }
 
   type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
-- 
cgit v1.2.3