From e2db603243dd5aae38497018c8c0cae732a8a8bb Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 21 May 2003 13:19:05 +0000 Subject: MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4048 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index a7c253577..2e66d182c 100644 --- a/CHANGES +++ b/CHANGES @@ -3,7 +3,7 @@ Changes from V7.4 A revision of the standard library and of concrete syntax of Coq, including -- a completely new syntax for terms +- a completely new syntax for terms coming with an automatic translator - renaming of various standard notions from French to English (esp in ZArith) - notions of the standard library are declared with (strict) implicit arguments - eq merged with eqT: old eq disappear, new eq (written =) is old eqT @@ -13,6 +13,18 @@ A revision of the standard library and of concrete syntax of Coq, including - a additional elimination Acc_iter for Acc, simplier than Acc_rect. This new elimination principle is used for definition well_founded_induction. +Syntax translator + +- Unsafe for annotation Cases when constructors coercions are used or when + annotations are eta-reduced predicates +- Recursive keyword set by default (and no longer needed) in Tactic Definition + +Syntax for arithmetic + +- Notation "=" and "<>" in Z and R are no longer implicitly in Z or R + (with possible introduction of a coercion), use ...=... or + ...<>... instead + Vernacular commands - "Declare ML Module" now allows us to import .cma files. This avoids to use a @@ -39,8 +51,15 @@ Grammar extensions - UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F (letter-like, including aleph and double N,Z,Q,R) are supported identifiers; UTF-8 unicode blocs 2200-22FF (mathematical operators), - 2300-23FF (miscellaneous technical, including sqrt symbol) and - 2600-26FF (miscellaneous symbols) are supported symbols + 2A00-2AFF (supplemental mathematical operators) 2300-23FF + (miscellaneous technical, including sqrt symbol), 2600-26FF + (miscellaneous symbols) 2190-21FF (arrows A) and 2900-297F (arrows B) + are supported symbols + +Library + +- New file about the factorial function in Arith +- Variables names of iff_trans changed (source of incompatibilities) Tactic language @@ -53,10 +72,14 @@ Tactics if the right-hand-side of "Match term With" are tactics, these tactics are never evaluated immediately and do not induce backtracking (in contrast with "Match Context") +- Quantified names now avoid global names of the current module (like + Intro names did) [source of rare incompatibilities: 2 changes in the set of + user contribs] Bugs - Rename bug fixed (#244) +- see coq-bugs server for the complete list of fixed bugs Changes from V7.3.1 to V7.4 =========================== -- cgit v1.2.3