From fb77937a6ba0fe45e978911db08de57f931683e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Dec 2015 23:38:00 +0100
Subject: Changing syntax of pat/constr1.../constrn into
 pat%constr1...%constrn. Marking it as experimental.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 70ed1bef01..389572014e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,9 @@ Tactics
 
 - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
   for induction.
+- Syntax "p/c" for on-the-fly application of a lemma c before
+  introducing along pattern p changed to p%c1..%cn. The feature and
+  syntax are in experimental stage.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
-- 
cgit v1.2.3


From 119d61453c6761f20b8862f47334bfb8fae0049e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 11 Dec 2015 12:17:14 +0100
Subject: Document removal of Set Virtual Machine and -vm in CHANGES.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 389572014e..f31f4efa88 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,7 @@ Vernacular commands
   declaration of all polymorphic universes appearing in a definition when
   introducing it.
 - New command "Show id" to show goal named id.
+- Option "Virtual Machine" removed.
 
 Tactics
 
@@ -82,6 +83,7 @@ Tools
 - The -require and -load-vernac-object command-line options now take a logical
   path of a given library rather than a physical path, thus they behave like
   Require [Import] path.
+- The -vm command-line option has been removed.
 
 Standard Library
 
-- 
cgit v1.2.3