From 2cf2a943e7140e50343bcb7d2eab24bebeeea9ec Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 19 Mar 2012 17:48:55 +0000
Subject: 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
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 4a5c744104..a12caacba2 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
 =============================
-- 
cgit v1.2.3