diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-27 21:00:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-27 21:00:30 +0000 |
| commit | 0acacf898cf1c761051eb168743134326eee84b8 (patch) | |
| tree | acfd5a3555af850bc3fa737b44a447a44411422d /CHANGES | |
| parent | 84140c29194446cc62f0024ea916cb530c329e46 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5392 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -12,6 +12,7 @@ Syntax - Command "Print." discontinued. - "assert" semantics now consistent with reference manual - Redundant syntax "Implicit Arguments On/Off" discontinued +- Delimiting key %bool for bool_scope added Interpretation scopes @@ -34,9 +35,10 @@ Bug fixes - Fix pattern-matching compilation bugs (and new support for patterns in a same column but in different inductive types) - Fix a potential precedence problem with notations including pattern "{ _ }" +- Fix an incorrect numbering of occurrences in "simpl id at num" - Fix nested coercion printing bug - Fix printing of notation when interleaved with coercions -- Fix "Tactic Notation" translation bugs +- Fix "Tactic Notation" translation bugs and improve file location of errors Changes from V8.0beta old syntax to V8.0beta ============================================ |