From d3127693d4a2125088aa512f593d782843482f2a Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 16:09:11 +0000
Subject: [vernac] use plain strings as attribute names

The concrete syntax is still restricted to identifiers.
---
 vernac/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/vernacexpr.ml')

diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2287630c7..e97cac818 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -459,7 +459,7 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = (Names.Id.t * vernac_flag_value) list
+type vernac_flags = (string * vernac_flag_value) list
 and vernac_flag_value =
   | VernacFlagEmpty
   | VernacFlagLeaf of string
-- 
cgit v1.2.3