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/funind/g_indfun.ml4 | 2 +-
 plugins/ssr/ssrvernac.ml4   | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 829556a71e..87609296bc 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+             (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
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