From 790c8a5d77eaecaa02b6fd9e1ce769c08ce905fa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Dec 2002 18:02:24 +0000
Subject: Prise en compte des coercions dans les 'with' bindings

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 2087d1793b..22ac7b0132 100644
--- a/CHANGES
+++ b/CHANGES
@@ -86,8 +86,7 @@ Tactics
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
-- New syntax for Ring and Field when arguments are provided (use "Ring on" and
-  "Field on")
+- Coercions now handled in "with" bindings
 
 Miscellaneous
 
-- 
cgit v1.2.3