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