From bdf8f3cfac1542cb2f052833a21ab00a715babe9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Dec 2005 15:11:06 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7685 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 7b8b5b5970..f2a887cb0f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -49,6 +49,8 @@ Tactics
   ~B |- A and ~A |- B respectively.
 - Added command "Declare Implicit Tactic" to set up a default tactic to be
   used to solve unresolved subterms of term arguments of tactics.
+- Better support for coercions to Sortclass in tactics expecting type arguments
+- Low-priority term printer made available in ML-written tactic extensions
 
 Modules
 
@@ -65,6 +67,7 @@ Modules
 Notations
 
 - "format" option aware of recursive notations
+- no more automatic printing box in case of user-provided printing "format"
 
 Library
 
-- 
cgit v1.2.3