More adaptations of pretyping/coercion to Program mode.

- (Regular) Casts become typing constraints again.
- Coerce tycon to inductive type when applying bidirectional typechecking hint.
- Coerce lambda expressions to tycon, might require coercions now.

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

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4a5c74410..a12caacba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,8 +4,11 @@ Changes from V8.4
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
+
+Program
 - "Solve Obligations using" changed to "Solve Obligations with",
   consistent with "Proof with".
+- Program Lemma, Definition now respect automatic introduction.
 
 Changes from V8.4beta to V8.4
 =============================