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.
---
 parsing/g_proofs.ml4 | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'parsing/g_proofs.ml4')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f10d746770..d88f6fa0dc 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -70,19 +70,16 @@ GEXTEND Gram
 	    VernacCreateHintDb (id, b)
       | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
 	  VernacRemoveHints (dbnames, ids)
-      | IDENT "Hint"; local = obsolete_locality; h = hint;
+      | IDENT "Hint"; h = hint;
 	  dbnames = opt_hintbases ->
-	  VernacHints (local,dbnames, h)
+          VernacHints (dbnames, h)
       (* Declare "Resolve" explicitly so as to be able to later extend with
          "Resolve ->" and "Resolve <-" *)
       | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
 	info = hint_info; dbnames = opt_hintbases ->
-	  VernacHints (false,dbnames,
+          VernacHints (dbnames,
 	    HintsResolve (List.map (fun x -> (info, true, x)) lc))
       ] ];
-  obsolete_locality:
-    [ [ IDENT "Local" -> true | -> false ] ]
-  ;
   reference_or_constr:
    [ [ r = global -> HintsReference r
      | c = constr -> HintsConstr c ] ]
-- 
cgit v1.2.3