From d03f3905c44e3b1582bd77e23203dc45e5e02041 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jun 2006 18:29:40 +0000
Subject: replace by

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

diff --git a/CHANGES b/CHANGES
index 7763341ecf..b0945ed0cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -81,6 +81,7 @@ Tactics
 - Better support for coercions to Sortclass in tactics expecting type arguments
 - Low-priority term printer made available in ML-written tactic extensions
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
+- Tactic "replace" now accepts a "by" tactic clause
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
 - New introduction pattern "?" for letting Coq choose a name
 - Added "eassumption"
-- 
cgit v1.2.3