Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

1 files changed, 33 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 87506dadc1..d2890f7402 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,39 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 
+Tactics
+
+- New flag "Regular Subst Tactic" which fixes "subst" in situations where
+  it failed to substitute all substitutable equations or failed to simplify
+  cycles, or accidentally unfolded local definitions (flag is off by default).
+- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a
+  special way. It accepts three distinct flags:
+  * "Lax", which is the default one, sets the old behavior, i.e. a non-imported
+  hint behaves the same as an imported one.
+  * "Warn" outputs a warning when a non-imported hint is used. Note that this is
+  an over-approximation, because a hint may be triggered by an eauto run that
+  will eventually fail and backtrack.
+  * "Strict" changes the behavior of an unloaded hint to the one of the fail
+  tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
+
+API
+
+- Some functions from pretyping/typing.ml and their derivatives were potential
+  source of evarmap leaks, as they dropped their resulting evarmap. The
+  situation was clarified by renaming them according to a unsafe_* scheme. Their
+  sound variant is likewise renamed to their old name. The following renamings
+  were made.
+  * Typing.type_of -> unsafe_type_of
+  * Typing.e_type_of -> type_of
+  * A new e_type_of function that matches the e_ prefix policy
+  * Tacmach.pf_type_of -> pf_unsafe_type_of
+  * A new safe pf_type_of function.
+  All uses of unsafe_* functions should be eventually eliminated.
+
+
+Tools
+
+- Added an option -w to control the output of coqtop warnings.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
@@ -19,7 +52,6 @@ Tactics
 - A script using the admit tactic can no longer be concluded by either
   Qed or Defined. In the first case, Admitted can be used instead. In
   the second case, a subproof should be used.
-
 - The easy tactic and the now tactical now have a more predictable
   behavior, but they might now discharge some previously unsolved goals.
 
@@ -27,25 +59,21 @@ Extraction
 
 - Definitions extracted to Haskell GHC should no longer randomly
   segfault when some Coq types cannot be represented by Haskell types.
-
 - Definitions can now be extracted to Json for post-processing.
 
 Tools
 
 - Option -I -as has been removed, and option -R -as has been
   deprecated. In both cases, option -R can be used instead.
-
 - coq_makefile now generates double-colon rules for rules such as clean.
 
 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
 ==============================