aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2003-01-31 16:50:44 +0000
committerherbelin2003-01-31 16:50:44 +0000
commitaf47241eca486b4b80b76bf33ee60327041ba921 (patch)
tree6a9f0d1a0e701b71d6ef6a565070db77dcfd9348
parent253e5c3e2fe8815a15b55728039d789298166137 (diff)
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3639 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index b432e0ccdf..f6e98fc9e0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -151,6 +151,7 @@ Bugs
- Inversion bugs fixed (#212 and #220)
- Omega bug related to Set fixed (#180)
- Type-checking inefficiency of nested destructuring let-in fixed (#216)
+- Improved handling of let-in during holes resolution phase
Changes from V7.3 to V7.3.1
===========================