aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorherbelin2010-06-28 07:27:39 +0000
committerherbelin2010-06-28 07:27:39 +0000
commitab866bcd9b20dd5c6a2fed6978b77189c19f19f4 (patch)
tree2aa8ca1702f2c33cee443874a61bf190aca385a0 /CHANGES
parentf5458f9064be5cc4f645019df6519b265281a280 (diff)
Made "replace" accepts open terms on its left-hand-side.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13206 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index b53ad69725..bd0f4a1346 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,6 +25,7 @@ Rewriting tactics
by importing "Morphisms" too).
- Support added for using Chung-Kil Hur's Heq library for rewriting over
heterogeneous equality (courtesy of the library's author).
+- Tactic "replace" supports matching terms with holes.
Automation tactics