From ae5944b360c1e181fa162d7d6dced7e671c6fbe6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 12 Sep 2017 17:26:53 +0200
Subject: Remove "obsolete_locality" and fix STM vernac classification.

We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.

We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.

This is a preliminary step for the work on attributes.
---
 plugins/ssr/ssrvernac.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7385ed84c7..3efb7b9147 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
 
-- 
cgit v1.2.3