aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-12 17:26:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-29 16:12:14 +0100
commitae5944b360c1e181fa162d7d6dced7e671c6fbe6 (patch)
treeca5f2c680d0cd33028e75a579d5ffca31e83d6b0 /CHANGES
parentb23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff)
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.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 7a326c589..6a7a5a42b 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
===============================