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/ssr/ssrvernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 2f44624d36..2774b843aa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -173,7 +173,7 @@ VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
   | [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
          let open Attributes in
-         let locality = Locality.make_section_locality atts.locality in
+         let locality = Locality.make_section_locality (only_locality atts) in
          List.iter (declare_one_prenex_implicit locality) fl;
      }
 END
-- 
cgit v1.2.3