aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-03-07 21:39:55 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-03-07 21:39:55 +0000
commitd2562604fcea7ef0b0c5658af8fe21003ef3953e (patch)
tree7fde3fe8bac6e069de13a153fda8844bd98a3a04 /CHANGES
parent3af4fe78c8e5ed1c4148e8feeffeb6c66eaa6b09 (diff)
Added 'clear - id' to clear all hypotheses except the ones dependent in the statement of id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 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 8104f54eb..25eb039ff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,7 @@ Ltac
Tactics
+- Added "clear - id" to clear all hypotheses except the ones depending in id.
- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
- The argument of Declare Left Step and Declare Right Step is now a term
(it used to be a reference) (doc TODO)