Merge branch 'v8.5'

1 files changed, 12 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index a279e487ea..2cc91bbd6b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,14 +12,15 @@ Program
 - The "Shrink Obligations" flag now applies to all obligations, not only those
   solved by the automatic tactic.
 
-Changes from V8.5beta3
-======================
+Changes from V8.5beta3 to V8.5
+==============================
 
-Vernacular commands
-- Flag -compat 8.4 now loads Coq.Compat.Coq84. The standard way of putting Coq
-  in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It
-  can be followed by "-require Coq.Compat.AdmitAxiom" if 8.4 behavior of admit is
-  needed, in which case it uses an axiom.
+Tools
+
+- Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of
+  putting Coq in v8.4 compatibility mode is to pass the command line flag
+  "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom"
+  if the 8.4 behavior of admit is needed, in which case it uses an axiom.
 
 Specification language
 
@@ -34,6 +35,10 @@ Tactics
 - 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.
+- "Proof using" does not clear unused section variables.
+- "refine" has been changed back to the 8.4 behavior of shelving subgoals
+  that occur in other subgoals. The "refine" tactic of 8.5beta2 has been
+  renamed "simple refine"; it does not shelve any subgoal.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================