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/firstorder/g_ground.mlg | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 14a3acad57..b9274cf6b8 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -20,6 +20,7 @@ open Tacticals.New
 open Tacinterp
 open Stdarg
 open Tacarg
+open Attributes
 open Pcoq.Prim
 
 }
@@ -73,10 +74,9 @@ let (set_default_solver, default_solver, print_default_solver) =
 }
 
 VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
-| [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
-    let open Attributes in
+| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
       set_default_solver
-        (Locality.make_section_locality (only_locality atts))
+        (Locality.make_section_locality locality)
         (Tacintern.glob_tactic t)
   }
 END
-- 
cgit v1.2.3