aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-19 14:53:37 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-19 14:53:37 +0000
commita1440ee74b14532cad3e49d518336ed336e0b137 (patch)
treea1ef7e3620386c324e52841aac253155b9f3f1fc /CHANGES
parent4c42efa7cbea5b70e2b78a023f9d5b667f87f789 (diff)
Export eassumption
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 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 4d1e687f0..d9adabaf7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,7 @@ Tactics
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- New introduction pattern "?" for letting Coq choose a name
+- Added "eassumption"
Modules