Fix bugs related to Program integration.

- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b587e2ecc..4a5c74410 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,8 @@ Changes from V8.4
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
+- "Solve Obligations using" changed to "Solve Obligations with",
+  consistent with "Proof with".
 
 Changes from V8.4beta to V8.4
 =============================