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/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 940defb743..2f44624d36 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -172,7 +172,7 @@ let declare_one_prenex_implicit locality f =
 VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
   | [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
-         let open Vernacinterp in
+         let open Attributes in
          let locality = Locality.make_section_locality atts.locality in
          List.iter (declare_one_prenex_implicit locality) fl;
      }
-- 
cgit v1.2.3