aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorherbelin2006-02-07 19:02:31 +0000
committerherbelin2006-02-07 19:02:31 +0000
commit403d742303d614d1dfa32b0ad4f61757af67fb17 (patch)
treea765a2f3266e7bd54102627321dd8ed0707e98c9 /CHANGES
parent129417d5ef8a8b73a836e92d1074aedc15cc9bbb (diff)
Mise en conformité de l'ordre des occurrences de pattern avec l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 60be31c2c4..48d59df054 100644
--- a/CHANGES
+++ b/CHANGES
@@ -65,6 +65,9 @@ Tactics
- New introduction pattern "?" for letting Coq choose a name
- Added "eassumption"
- Added option 'using lemmas' to auto, trivial and eauto
+- Numbering of "pattern" occurrences in "match with" made consistent
+ with the printing of the return clause after the term to match in
+ "match-with" construct (use "Set Printing All" to see hidden occurrences).
Modules