Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

1 files changed, 47 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 494575fa..4bc0bd82 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,50 @@
+Changes from V8.2 to forthcoming V8.2pl1
+========================================
+
+Language and commands
+
+- Fixing Not_found bug in Theorem with.
+- Fixing pattern parsing bug #2087.
+- Fixing name aliases bug #2085 with modules.
+- Fixing checker bug #2065 with -impredicative-set option.
+- Complying with 8.1 heuristic when unification returns several solutions.
+- Add [Print Opaque Dependencies] command to print the assumptions and 
+  the opaque constants a definition uses.
+- Fixing performance issue in Program's type inference when there are
+  many existentials.
+- Fixing bug #2093, using Program does not require to import Program.Tactics
+  anymore, it will use [idtac] as the default obligation tactic.
+- Fix imports when requiring Setoid, to avoid cluttering the context with
+  internal names (possible source of incompatibility, import Morphisms to fix).
+- Fixing bug #2089, Combined Scheme was not treating parameters correctly.
+- Fixing Program to use hooks correctly, when called through [Program Coercion]
+  for example.
+- Fixing manual implicit arguments to always work and remove 
+  [Set Manual Implicit Arguments] option (possible source of incompatibility).
+- Fixing refine to work with typeclasses.
+- Fixing implementation of [Context] to discharge class instances only on definitions
+  using some of the parameters or the instance itself (possible source of 
+  incompatibility).
+
+Tactics
+
+- Fixing correct binding of quantified hypotheses for induction/destruction
+  when used in Ltac.
+- Fixing bad parentheses check in "pose (f binders := ...)" syntax.
+- Fixing unbalanced parenthesis in Ltac debug trace printer.
+- Fixing missing sort unification check in lemma application (bug #2084).
+- Fixing "as" clause of "apply in" that was not working in the general case.
+- Fixing eauto not using external hints with no pattern.
+
+Tools and development
+
+- Fixing missing -c option in coq_makefile.
+- Temporary hack for coqide.byte "double free or corruption" problem.
+- Added support for code development under Bazaar.
+- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
+- Parsing fixes and support for parsing regular comments inline in coqdoc,
+  using option -parse-comments (suggestions by B. Pierce).
+
 Changes from V8.1 to V8.2
 =========================