From 58452e2b0a9847b6bd89941051dc2a0633679f6e Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 18 Aug 2011 15:08:00 +0000 Subject: Updates in CHANGES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14416 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 92 +++++++++++++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 75 insertions(+), 17 deletions(-) diff --git a/CHANGES b/CHANGES index 8d0623f585..ef5d8345be 100644 --- a/CHANGES +++ b/CHANGES @@ -23,7 +23,10 @@ Specification language and notations Tactics -- New proof engine supporting bullets. +- New proof engine. +- Scripts can now be structured thanks to bullets - * + and to subgoal + delimitation via { }. Note : for use with ProofGeneral, a cvs version of + ProofGeneral no older than mid-July 2011 is currently required. DOC TODO. - Support for tactical "info" is suspended. - Support for command "Show Script" is suspended. - New tactics constr_eq, is_evar and has_evar. @@ -44,7 +47,13 @@ Tactics Vernacular commands +- It is now mandatory to have a space (or tabulation or newline or end-of-file) + after a "." ending a sentence. - In SearchAbout, the [ ] delimiters are now optional. +- New command "Add/Remove Search Blacklist ..." : + a Search or SearchAbout or similar query will never mention lemmas + whose qualified names contain any of the declared substrings. + The default blacklisted substrings are "_admitted" "_subproof" "Private_". DOC TODO - When the output file of "Print Universes" ends in ".dot" or ".gv", the universe graph is printed in the DOT language, and can be processed by Graphviz tools. @@ -57,6 +66,10 @@ Vernacular commands Module System +- During subtyping checks, an opaque constant in a module type could now + be implemented by anything of the right type, even if bodies differ. + Said otherwise, with respect to subtyping, an opaque constant behaves + just as a parameter. Coqchk was already implementing this, but not coqtop. - The inlining done during application of functors can now be controlled more precisely, by the annotations (no inline) or (inline at level XX). With the latter annotation, only functor parameters whose levels @@ -64,21 +77,51 @@ Module System The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. TODO: DOC! +- Print Module (Type) now tries to print more details, such as types and + bodies of the module elements. Note that Print Module Type could be + used on a module to display only its interface. The option + "Set Short Module Printing" could be used to switch back to the earlier + behavior were only field names were displayed. Libraries -- Creation of PArith, a subdirectory containing files about the positive type, - such as BinPos or Pnat. - Extension of the abstract part of Numbers, which now provide axiomatizations - and results about many more functions, such as pow, gcd, lcm, sqrt, log2. - Implementations of these functions in nat N BigN Z BigZ. See in particular - Npeano for new functions about nat. -- Important revision of NArith and ZArith. In particular some definitions - or lemmas may have moved. The alternative division (Trunc convention - instead of Floor) is now named Zquot (noted ÷) and Zrem by analogy - with Haskell. In Zeven, the behavior of Zdiv2 on negative numbers has been - changed to be consistent with Zdiv, while the old behavior now corresponds - to function Zquot2. TODO: say more later. + and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2 + and bitwise functions. These functions are implemented for nat N BigN Z BigZ. + See in particular file NPeano for new functions about nat. +- The definition of types positive, N, Z is now in file BinNums.v +- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains + an internal module Z implementing the Numbers interface for integers. + This module Z regroups: + * all functions over type Z : Z.add, Z.mul, ... + * the minimal proofs of specifications for these functions : Z.add_0_l, ... + * an instantation of all derived properties proved generically in Numbers : + Z.add_comm, Z.add_assoc, ... + A large part of ZArith is now simply compatibility notations, for instance + Zplus_comm is an alias for Z.add_comm. The direct use of module Z is now + recommended instead of relying on these compatibility notations. +- Similar major reorganization of NArith, via a module N in NArith/BinNat.v +- Concerning the positive datatype, BinPos.v is now in a specific directory + PArith, and contains an internal submodule Pos. We regroup there functions + such as Pos.add Pos.mul etc as well as many results about them. These results + are here proved directly (no Number interface for strictly positive numbers). +- Note that in spite of the compatibility layers, all these reorganizations + may induce some marginal incompatibilies in scripts. In particular: + * the "?=" notation for positive now refers to a binary function Pos.compare, + instead of the infamous ternary Pcompare (now Pos.compare_cont). + * some hypothesis names generated by the system may changed (typically for + a "destruct Z_le_gt_dec") since naming is done after the short name of + the head predicate (here now "le" in module Z instead of "Zle", etc). + * the internals of Z.add has changed, now relying of Z.pos_sub. +- Also note these new notations: + * "= XP SP1. +- The Coqide parsing of sentences has be reworked and now supports + tactic delimitation via { }. +- Coqide now accepts the Abort command (wish #2357). + +Tools + +- Coq now searches directories specified in COQPATH and user-contribs before + the standard library. - coq_makefile major cleanup. * mli taken into account, ml not preproccessed anymore, ml4 work * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR -- cgit v1.2.3