aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrvernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index c0479dd24..d74ad06b3 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