aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrvernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrvernac.ml4')
-rw-r--r--plugins/ssr/ssrvernac.ml46
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7385ed84c..3efb7b914 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -551,9 +551,9 @@ GEXTEND Gram
| IDENT "Canonical"; qid = Constr.global;
d = G_vernac.def_body ->
let s = coerce_reference_to_id qid in
- Vernacexpr.VernacDefinition
- ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
- ((Loc.tag s),None),(d ))
+ Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition
+ ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
+ ((Loc.tag s),None),(d )))
]];
END