From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2015 11:28:44 +0200
Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080

This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)).  It is
useful to have function_scope for, e.g., function composition.  This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.

Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax.  (The scope type_scope
should not be special-cased; this change is coming up next.)

Also explicitly define [function_scope] in theories/Init/Notations.v.

This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]

We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 08484a4b9b..12ee5d27fc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,9 @@ Tactics
   let tactics working under conjunctions apply sublemmas of the form
   "forall A, ... -> A".
 
+Notations
+- "Bind Scope" can once again bind "Funclass" and "Sortclass".
+
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential
-- 
cgit v1.2.3


From 498cbad3e5e5d69d2ee771f90de45c0fe28cc494 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Sep 2015 18:19:50 +0200
Subject: Explain new flags for native_compute in CHANGES.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 70ddb81f4d..c8fca217fd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -46,6 +46,11 @@ API
 Tools
 
 - Added an option -w to control the output of coqtop warnings.
+- Configure now takes an optional -native-compiler (yes|no) flag replacing
+  -no-native-compiler. The new flag is set to no by default under Windows.
+- Flag -no-native-compiler was removed and became the default for coqc. If
+  precompilation of files for native conversion test is desired, use
+  -native-compiler.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
-- 
cgit v1.2.3


From 3930c586507bfb3b80297d7a2fdbbc6049aa509b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Sep 2015 19:13:30 +0200
Subject: Updating the documentation and the toolchain w.r.t. the change in
 -compile.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index c8fca217fd..e3224db048 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,9 @@ Tools
 - Flag -no-native-compiler was removed and became the default for coqc. If
   precompilation of files for native conversion test is desired, use
   -native-compiler.
+- The -compile command-line option now takes the full path of the considered
+  file, including the ".v" extension, and outputs a warning if such an extension
+  is lacking.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
-- 
cgit v1.2.3


From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Sep 2015 12:25:35 +0200
Subject: The -require option now accepts a logical path instead of a physical
 one.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index e3224db048..950f2fab18 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,8 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
+- The -require command-line option now takes a logical path of a given library
+  rather than a physical path.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
-- 
cgit v1.2.3


From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Sep 2015 11:04:59 +0200
Subject: Make -load-vernac-object respect the loadpath.

This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.

This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
---
 CHANGES | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 950f2fab18..16d86c8ff1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,8 +54,9 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
-- The -require command-line option now takes a logical path of a given library
-  rather than a physical path.
+- 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.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
-- 
cgit v1.2.3


From 27d4a636cb7f1fbdbced1980808a9b947405eeb5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 7 Oct 2015 23:08:45 +0200
Subject: Remove the "exists" overrides from Program. (Fix bug #4360)

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 16d86c8ff1..cf2bb49271 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ Tactics
   "intros" automatically complete the introduction of its subcomponents, as the
   the disjunctive-conjunctive introduction patterns in non-terminal position
   already do.
+- Importing Program no longer overrides the "exists" tactic (potential source
+  of incompatibilities).
 
 API
 
-- 
cgit v1.2.3


From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index cf2bb49271..07d129a462 100644
--- a/CHANGES
+++ b/CHANGES
@@ -2180,7 +2180,7 @@ Changes from V7.3.1 to V7.4
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
-  a notation sets has been developped for nat, Z and R (undocumented)
+  a notation sets has been developed for nat, Z and R (undocumented)
 - New command "Notation" for declaring notations simultaneously for
   parsing and printing (see chap 10 of the reference manual)
 - Declarations with only implicit arguments now handled (e.g. the
-- 
cgit v1.2.3


From 289dde7331ee19229b9ba4b9778a76007d93b275 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Oct 2015 10:55:19 +0200
Subject: Documenting the option "Strict Universe Declaration" in CHANGES.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 07d129a462..9f46131363 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,9 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 - New command "Undelimit Scope" to remove the delimiter of a scope.
+- New option "Strict Universe Declaration", set by default. It enforces the
+  declaration of all polymorphic universes appearing in a definition when
+  introducing it.
 
 Tactics
 
-- 
cgit v1.2.3


From 95b04506542064fbda7a61c4b6ce276a668d25bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 21 Oct 2015 16:40:51 +0200
Subject: Mention bug 3199 fix as a source of incompatibilities.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 9f46131363..cf0f4446f4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -33,6 +33,9 @@ Tactics
   already do.
 - Importing Program no longer overrides the "exists" tactic (potential source
   of incompatibilities).
+- Hints costs are now correctly taken into account (potential source of
+  incompatibilities).
+
 
 API
 
-- 
cgit v1.2.3


From 4e643d134f02cfa9a73754c3cf48048541324834 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2015 15:49:09 +0100
Subject: Adding syntax "Show id" to show goal named id (shelved or not).

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index cf0f4446f4..019c6cdb24 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,7 @@ Vernacular commands
 - New option "Strict Universe Declaration", set by default. It enforces the
   declaration of all polymorphic universes appearing in a definition when
   introducing it.
+- New command "Show id" to show goal named id.
 
 Tactics
 
@@ -36,7 +37,6 @@ Tactics
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
 
-
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential
-- 
cgit v1.2.3


From acc54398bd244b15d4dbc396836c279eabf3bf6b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Nov 2015 13:37:10 -0500
Subject: Hint Cut documentation and cleanup of printing (was duplicated and
 inconsistent).

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 019c6cdb24..af874bf1cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
   of incompatibilities).
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
+- Documented the Hint Cut command that allows control of the
+  proof-search during typeclass resolution (see reference manual).
 
 API
 
-- 
cgit v1.2.3


From 0fd6ad21121c7c179375b9a50c3135abab1781b2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 5 Nov 2015 16:44:16 +0100
Subject: Update version numbers and magic numbers for 8.5beta3 release.

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index af874bf1cc..7b50dfae56 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,4 +1,4 @@
-Changes from V8.5beta2 to ...
+Changes from V8.5beta2 to V8.5beta3
 ===================================
 
 Vernacular commands
-- 
cgit v1.2.3


From bd1c976531ad6154339fff7e48e85dbe7951de23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2015 11:20:04 +0200
Subject: Activating bracketing of last or-and introduction pattern by default
 for more regularity.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5d6dd69c60..10ec10a5e4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,8 @@
+Changes beyond V8.5
+===================
+
+- Flag "Bracketing Last Introduction Pattern" is now on by default.
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
-- 
cgit v1.2.3


From 575fdab5df7c861692b19c62c2004c339c8621df Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2015 11:21:55 +0200
Subject: Listing separately changes from 8.5betas to final 8.5 and further
 changes from final 8.5 to next version.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 10ec10a5e4..91d5f0baa6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,7 +1,16 @@
 Changes beyond V8.5
 ===================
 
+Tactics
+
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
+- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
+  tactical w.r.t. variables appearing in the body of the proof.
+
+Program
+
+- The "Shrink Obligations" flag now applies to all obligations, not only those
+  solved by the automatic tactic.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
-- 
cgit v1.2.3


From 67da4b45ef65db59b2d7ba1549351d792e1b27d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:15:37 -0500
Subject: Fix bug #3735: interpretation of "->" in Program follows the standard
 one.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 7b50dfae56..f67c34b81b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -397,6 +397,9 @@ Program
 - "Solve Obligations using" changed to "Solve Obligations with",
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
+- Program Lemma, Definition, etc.. now interpret "->" like Lemma and
+  Definition as a non-dependent arrow (potential source of
+  incompatibility).
 - Add/document "Set Hide Obligations" (to hide obligations in the final
   term inside an implicit argument) and "Set Shrink Obligations" (to
   minimize dependencies of obligations defined by tactics).
-- 
cgit v1.2.3


From 69ed7f0ac9d651eaab85153ea55f5c7d9bf6ae20 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 11 Nov 2015 18:14:40 -0500
Subject: Update CHANGES

Mention compatibility file.
---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index f67c34b81b..719be44929 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,13 @@ Tools
   path of a given library rather than a physical path, thus they behave like
   Require [Import] path.
 
+Standard Library
+
+ - There is now a Coq.Compat.Coq84 library, which sets the various compatibility
+   options and does a few redefinitions to make Coq behave more like Coq v8.4.
+   The standard way of putting Coq in v8.4 compatibility mode is to pass the command
+   line flags "-require Coq.Compat.Coq84 -compat 8.4".
+
 Changes from V8.5beta1 to V8.5beta2
 ===================================
 
-- 
cgit v1.2.3


From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 19 Nov 2015 17:48:32 +0100
Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a
 constr, and the associated signature, not needed anymore. Update CHANGES, no
 evar_map is produced by pattern_of_constr anymore.

---
 CHANGES | 2 --
 1 file changed, 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 719be44929..07d6281717 100644
--- a/CHANGES
+++ b/CHANGES
@@ -107,8 +107,6 @@ API
 
 - The interface of [change] has changed to take a [change_arg], which
   can be built from a [constr] using [make_change_arg].
-- [pattern_of_constr] now returns a triplet including the cleaned-up
-  [evar_map], removing the evars that were turned into metas.
 
 Changes from V8.4 to V8.5beta1
 ==============================
-- 
cgit v1.2.3


From 9205d8dc7b9e97b6c2f0815fddc5673c21d11089 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Nov 2015 12:26:53 +0100
Subject: Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in
 WG.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 07d6281717..662b7b9a24 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,10 @@ Vernacular commands
   introducing it.
 - New command "Show id" to show goal named id.
 
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
 Tactics
 
 - New flag "Regular Subst Tactic" which fixes "subst" in situations where
@@ -83,6 +87,10 @@ Logic
 - The VM now supports inductive types with up to 8388851 non-constant
   constructors and up to 8388607 constant ones.
 
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
 Tactics
 
 - A script using the admit tactic can no longer be concluded by either
-- 
cgit v1.2.3


From cbceffe424a6b4477eb822f3887776b587503cbd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 00:42:24 +0100
Subject: Fix CHANGES.

---
 CHANGES | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 662b7b9a24..96f02bc27c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,10 @@
+Changes from V8.5beta3
+======================
+
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac:(tactic)".
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
@@ -10,10 +17,6 @@ Vernacular commands
   introducing it.
 - New command "Show id" to show goal named id.
 
-Specification language
-
-- Syntax "$(tactic)$" changed to "ltac: tactic".
-
 Tactics
 
 - New flag "Regular Subst Tactic" which fixes "subst" in situations where
-- 
cgit v1.2.3


From 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 00:14:37 +0100
Subject: Changing "destruct !hyp" into "destruct (hyp)" (and similarly for
 induction) based on a suggestion of Guillaume M. (done like this in
 ssreflect).

This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 96f02bc27c..70ed1bef01 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,11 @@ Specification language
 
 - Syntax "$(tactic)$" changed to "ltac:(tactic)".
 
+Tactics
+
+- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
+  for induction.
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
-- 
cgit v1.2.3


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


From c377938a8f87d9c0517aa0c7d4564323951a2133 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 13:19:09 +0100
Subject: Flag -compat 8.4 now loads Coq.Compat.Coq84.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index f31f4efa88..8cb5158753 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes from V8.5beta3
 ======================
 
+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.
+
 Specification language
 
 - Syntax "$(tactic)$" changed to "ltac:(tactic)".
-- 
cgit v1.2.3


From 317858b7ad05764a2ce010354631443f219a4b9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Dec 2015 12:03:45 +0100
Subject: Updating CHANGES with an incompatibility.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 8cb5158753..b39d84ba57 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,7 +14,9 @@ Specification language
 Tactics
 
 - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
-  for induction.
+  for induction (rare source of incompatibilities easily solvable by
+  removing parentheses around "hyp" when not for the purpose of keeping
+  the hypothesis).
 - 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.
-- 
cgit v1.2.3


From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 15 Dec 2015 23:15:02 +0100
Subject: Proof using: do not clear unused section hyps automatically

The option is still there, but not documented since it is too
dangerous.  Hints and type classes instances are not taking cleared
variables into account.
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b39d84ba57..a3cec81c1a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,7 @@ 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.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
-- 
cgit v1.2.3


From b8d1e84e9326df34383e5e5c8c5842cb7013b935 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 16 Dec 2015 18:30:32 +0100
Subject: Add a "simple refine" variant of "refine" that does not call
 "shelve_unifiable".

---
 CHANGES | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a3cec81c1a..df2fc967dd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,11 +1,12 @@
 Changes from V8.5beta3
 ======================
 
-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
 
@@ -21,6 +22,9 @@ Tactics
   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
 ===================================
-- 
cgit v1.2.3


From 8913baad8de063f5a215a342d04929ac75d75c28 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Dec 2015 22:28:35 +0100
Subject: Update version numbers and magic numbers for 8.5rc1 release.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index df2fc967dd..b30bcc662d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,5 @@
-Changes from V8.5beta3
-======================
+Changes from V8.5beta3 to V8.5
+==============================
 
 Tools
 
-- 
cgit v1.2.3


From 74d89e0be05e5cb4c9faf154478bc0c907bec2bb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Dec 2015 20:14:07 +0100
Subject: Reporting about the new tactical unshelve.

---
 CHANGES | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b30bcc662d..531d5049fd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,9 +22,11 @@ Tactics
   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
+- Tactic "refine" has been changed back to the 8.4 behavior of shelving subgoals
+  that occur in other subgoals. The "refine" tactic of 8.5beta3 has been
   renamed "simple refine"; it does not shelve any subgoal.
+- New tactical "unshelve tac" which grab existential variables put on
+  the tactic shelve by the execution of "tac".
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
@@ -495,11 +497,9 @@ Interfaces
   documentation of OCaml's Str module for the supported syntax.
 - Many CoqIDE windows, including the query one, are now detachable to
   improve usability on multi screen work stations.
-
 - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks
   to the COQ_COLORS environment variable, and their current state can
   be displayed with the -list-tags command line option.
-
 - Third party user interfaces can install their main loop in $COQLIB/toploop
   and call coqtop with the -toploop flag to select it.
 
-- 
cgit v1.2.3


From 4b075af747f65bcd73ff1c78417cf77edf6fbd76 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 01:13:56 +0100
Subject: Fixing some problems with double induction.

Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.

Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".

Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).

See file induct.v for effect of changes.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a9fbfe29d0..cda16d3804 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,10 @@ Tactics
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
+- Serious bugs are fixed in tactic "double induction" (source of
+  incompatibilities as soon as the inductive types have dependencies in
+  the type of their constructors; "double induction" remains however
+  deprecated).
 
 Program
 
-- 
cgit v1.2.3


From 9c2662eecc398f38be3b6280a8f760cc439bc31c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 01:43:10 +0100
Subject: Stronger invariants on the use of the introduction pattern
 (pat1,...,patn).

The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.

Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index cda16d3804..e80a3b4547 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,9 @@ Tactics
   incompatibilities as soon as the inductive types have dependencies in
   the type of their constructors; "double induction" remains however
   deprecated).
+- In introduction patterns of the form (pat1,...,patn), n should match
+  the exact number of hypotheses introduced (except for local definitions
+  for which pattern can be omitted, as in regular pattern-matching).
 
 Program
 
-- 
cgit v1.2.3


From d5656a6c28f79d59590d4fde60c5158a649d1b65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 11:16:03 +0100
Subject: Making parentheses mandatory in tactic scopes.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index e80a3b4547..ae055cb2f8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,8 @@ Tactics
 - In introduction patterns of the form (pat1,...,patn), n should match
   the exact number of hypotheses introduced (except for local definitions
   for which pattern can be omitted, as in regular pattern-matching).
+- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
+  their argument.
 
 Program
 
-- 
cgit v1.2.3


From cbc3a5f16871adb399689f7673a2a29a82dbf0cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 16:30:40 +0100
Subject: All arguments defined through ARGUMENT EXTEND declare a tactic scope.

Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ae055cb2f8..7de1015275 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Tactics
   for which pattern can be omitted, as in regular pattern-matching).
 - Tactic scopes in Ltac like constr: and ltac: now require parentheses around
   their argument.
+- Every generic argument type declares a tactic scope of the form "name:(...)"
+  where name is the name of the argument. This generalizes the constr: and ltac:
+  instances.
 
 Program
 
-- 
cgit v1.2.3


From 17c2147fe0a73b4e0af6481afd73df5cdcf8aefd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Apr 2016 15:47:34 +0200
Subject: Fix after merge, the revert of Bind Scope applies to trunk only.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 161906fd72..3f7cc7c98e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,10 @@ Program
 - The "Shrink Obligations" flag now applies to all obligations, not only those
   solved by the automatic tactic.
 
+Notations
+
+- "Bind Scope" can once again bind "Funclass" and "Sortclass".
+
 Changes from V8.5beta3 to V8.5
 ==============================
 
@@ -103,9 +107,6 @@ solved by the automatic tactic.
 - Documented the Hint Cut command that allows control of the
   proof-search during typeclass resolution (see reference manual).
 
-Notations
-- "Bind Scope" can once again bind "Funclass" and "Sortclass".
-
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential
-- 
cgit v1.2.3