From 0acacf898cf1c761051eb168743134326eee84b8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 27 Feb 2004 21:00:30 +0000 Subject: MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5392 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index 48d0c17082..666619f40b 100644 --- a/CHANGES +++ b/CHANGES @@ -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 ============================================ -- cgit v1.2.3