From ab8e47207245277cb5b92b80a92ae78ede5bfafe Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 12 Dec 2017 15:32:59 +0000
Subject: [vernac] vernac_expr no longer recursive

---
 plugins/ssr/ssrvernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4f530a0aec..c0479dd24b 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.VernacLocal(false,Vernacexpr.VernacDefinition
+    Vernacexpr.VernacDefinition
       ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((Loc.tag s),None),(d  )))
+          ((Loc.tag s),None), d)
   ]];
 END
 
-- 
cgit v1.2.3