aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrvernac.mlg2
1 files changed, 1 insertions, 1 deletions
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;
}