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.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 7a326c589a..6a7a5a42b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,6 +21,10 @@ Tactics
 - Tactic "decide equality" now able to manage constructors which
   contain proofs.
 
+Vernacular Commands
+- The deprecated Coercion Local, Open Local Scope, Notation Local syntax
+  was removed. Use Local as a prefix instead.
+
 Changes from 8.7+beta2 to 8.7.0
 ===============================
 
-- 
cgit v1.2.3