From e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 22 Jan 2018 08:26:17 +0000
Subject: [vernac] Remove VernacGoal, allow anonymous definitions in
 VernacDefinition

---
 plugins/ssr/ssrvernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index c0479dd24b..d74ad06b34 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -553,7 +553,7 @@ GEXTEND Gram
           let s = coerce_reference_to_id qid in
     Vernacexpr.VernacDefinition
       ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((Loc.tag s),None), d)
+          ((Loc.tag (Name s)),None), d)
   ]];
 END
 
-- 
cgit v1.2.3