From c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Sep 2018 14:14:03 +0200
Subject: Move attributes out of vernacinterp to new attributes module

---
 plugins/syntax/g_numeral.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 5dbc9eea7a..54764d541f 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -16,7 +16,7 @@ open Notation
 open Numeral
 open Pp
 open Names
-open Vernacinterp
+open Attributes
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
-- 
cgit v1.2.3


From 8db938764d87cceee6669b339e0f995edd40fc3e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Sep 2018 16:48:54 +0200
Subject: Command driven attributes.

Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.
---
 plugins/syntax/g_numeral.mlg | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 54764d541f..e70edd56cb 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -16,7 +16,6 @@ open Notation
 open Numeral
 open Pp
 open Names
-open Attributes
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -38,5 +37,5 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    { vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o }
+    { vernac_numeral_notation (Locality.make_module_locality (Attributes.only_locality atts)) ty f g (Id.to_string sc) o }
 END
-- 
cgit v1.2.3


From 0a478031f0213ef74c3649ea1a8d58aa89e54416 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 16 Oct 2018 14:42:53 +0200
Subject: coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax

I think for instance the new code in this diff is cleaner and more
systematic:
~~~diff
 VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
-| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
+| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
   } -> {
-         let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in
          Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
   }
 END
~~~
---
 plugins/syntax/g_numeral.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index e70edd56cb..13e0bcbd47 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -35,7 +35,7 @@ ARGUMENT EXTEND numnotoption
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-  | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    { vernac_numeral_notation (Locality.make_module_locality (Attributes.only_locality atts)) ty f g (Id.to_string sc) o }
+    { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
 END
-- 
cgit v1.2.3