diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 166 |
1 files changed, 104 insertions, 62 deletions
@@ -1,29 +1,66 @@ -Changes from V8.4beta to V8.4 -============================= +Changes from V8.4beta2 to V8.4 +============================== + +Vernacular commands + +- The "Reset" command is now supported again in files given to coqc or Load. +- "Show Script" now indents again the displayed scripts. It can also work + correctly across Load'ed files if the option "Unset Atomic Load" is used. +- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full + scope name (e.g. Z_scope). + +Notations + +- Most compatibility notations of the standard library are now tagged as + (compat xyz), where xyz is a former Coq version, for instance "8.3". + These notations behave as (only parsing) notations, except that they may + triggers warnings (or errors) when used while Coq is not in a corresponding + -compat mode. +- To activate these compatibility warnings, use "Set Verbose Compat Notations" + or the command-line flag -verbose-compat-notations. +- For a strict mode without these compatibility notations, use + "Unset Compat Notations" or the command-line flag -no-compat-notations. + +Tactics + +- An annotation "eqn:H" or "eqn:?" can be added to a "destruct" + or "induction" to make it generate equations in the spirit of "case_eq". + The former syntax "_eqn" is discontinued. +- The name of the hypothesis introduced by tactic "remember" can be + set via the new syntax "remember t as x eqn:H" (wish #2489). + +Libraries + +- Reals: changed definition of PI, no more axiom about sin(PI/2). +- SetoidPermutation: a notion of permutation for lists modulo a setoid equality. +- BigN: fixed the ocaml code doing the parsing/printing of big numbers. + +Changes from V8.4beta to V8.4beta2 +================================== Vernacular commands -- Undo and UndoTo are now handling the proof states. They may - perform some extra steps of backtrack to avoid states where - the proof state is unavailable (typically a closed proof). -- The commands Suspend and Resume have been removed. +- Commands "Back" and "BackTo" are now handling the proof states. They may + perform some extra steps of backtrack to avoid states where the proof + state is unavailable (typically a closed proof). +- The commands "Suspend" and "Resume" have been removed. - A basic Show Script has been reintroduced (no indentation). - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). -- New command "Grab Existential Variables" to transform the unresolved evars at - the end of a proof into goals. +- New command "Grab Existential Variables" to transform the unresolved evars + at the end of a proof into goals. Tactics -- Still no general "info" tactical, but new specific tactics - info_auto, info_eauto, info_trivial which provides information - on the proofs found by auto/eauto/trivial. Display of these - details could also be activated by Set Info Auto/Eauto/Trivial. -- Details on everything tried by auto/eauto/trivial during - a proof search could be obtained by "debug auto", "debug eauto", - "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". -- New command "r string" that interprets "idtac string" as a breakpoint - and jumps to its next use in Ltac debugger. +- Still no general "info" tactical, but new specific tactics info_auto, + info_eauto, info_trivial which provides information on the proofs found + by auto/eauto/trivial. Display of these details could also be activated by + "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial". +- Details on everything tried by auto/eauto/trivial during a proof search + could be obtained by "debug auto", "debug eauto", "debug trivial" or by a + global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial". +- New command "r string" in Ltac debugger that interprets "idtac + string" in Ltac code as a breakpoint and jumps to its next use. - Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy) have been removed, since Why2 has not been maintained for the last few years. The Why3 plugin should be a suitable @@ -31,28 +68,28 @@ Tactics Libraries -- MSetRBT : a new implementation of MSets via Red-Black trees (initial +- MSetRBT: a new implementation of MSets via Red-Black trees (initial contribution by Andrew Appel). -- MSetAVL : for maximal sharing with the new MSetRBT, the argument order - of Node has changed (this should be transparent to regular MSets users). +- MSetAVL: for maximal sharing with the new MSetRBT, the argument order + of Node has changed (this should be transparent to regular MSets users). Module System - The names of modules (and module types) are now in a fully separated - namespace from ordinary definitions : "Definition E:=0. Module E. End E." + namespace from ordinary definitions: "Definition E:=0. Module E. End E." is now accepted. CoqIDE -- Coqide now supports the Restart command, and Undo (with a warning). - Better support for Abort. +- Coqide now supports the "Restart" command, and "Undo" (with a warning). + Better support for "Abort". Changes from V8.3 to V8.4beta ============================= Logic -- Standard eta-conversion now supported (dependent product only). (DOC TO DO) +- Standard eta-conversion now supported (dependent product only). - Guard condition improvement: subterm property is propagated through beta-redex blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x"; this allows for instance to use "rewrite ... in ..." without breaking @@ -69,10 +106,6 @@ Specification language and notations - Structure/Record printing can be disable by "Unset Printing Records". In addition, it can be controlled on type by type basis using "Add Printing Record" or "Add Printing Constructor". -- In a pattern containing a "match", a final "| _ => _" branch could be used - now instead of enumerating all remaining constructors. Moreover, the pattern - "match _ with _ => _ end" now allows to match any "match". A "in" annotation - can also be added to restrict to a precise inductive type. - Pattern-matching compilation algorithm: in "match x, y with ... end", possible dependencies of x (or of the indices of its type) in the type of y are now taken into account. @@ -81,11 +114,11 @@ Tactics - 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. + delimitation via { }. Note: for use with Proof General, a cvs version of + Proof General no older than mid-July 2011 is currently required. - Support for tactical "info" is suspended. - Support for command "Show Script" is suspended. -- New tactics constr_eq, is_evar and has_evar. +- New tactics constr_eq, is_evar and has_evar for use in Ltac. - Removed the two-argument variant of "decide equality". - New experimental tactical "timeout <n> <tac>". Since <n> is a time in second for the moment, this feature should rather be avoided @@ -98,14 +131,14 @@ Tactics ?f x y = g(x,y) (compatibility ensured by using "Unset Tactic Pattern Unification"). It also supports (full) betaiota. - Tactic autorewrite does no longer instantiate pre-existing - existential variables (theoretical source of possible incompatibility). + existential variables (theoretical source of possible incompatibilities). - Tactic "dependent rewrite" now supports equality in "sig". - Tactic omega now understands Zpred (wish #1912) and can prove any goal from a context containing an arithmetical contradiction (wish #2236). - Using "auto with nocore" disables the use of the "core" database (wish #2188). This pseudo-database "nocore" can also be used with trivial and eauto. - Tactics "set", "destruct" and "induction" accepts incomplete terms and - use the goal to complete the pattern assuming it is no ambiguous. + use the goal to complete the pattern assuming it is non ambiguous. - When used on arguments with a dependent type, tactics such as "destruct", "induction", "case", "elim", etc. now try to abstract automatically the dependencies over the arguments of the types @@ -118,18 +151,25 @@ Tactics - When applying destruct or inversion on a fixpoint hiding an inductive type, recursive calls to the fixpoint now remain folded by default (rare source of incompatibility generally solvable by adding a call to simpl). -- The behavior of the simpl tactic can be tuned using the new "Arguments" - vernacular. +- In an ltac pattern containing a "match", a final "| _ => _" branch could be + used now instead of enumerating all remaining constructors. Moreover, the + pattern "match _ with _ => _ end" now allows to match any "match". A "in" + annotation can also be added to restrict to a precise inductive type. +- The behavior of "simpl" can be tuned using the "Arguments" vernacular. + In particular constants can be marked so that they are always/never unfolded + by "simpl", or unfolded only when a set of arguments evaluates to a + constructor. Last one can mark a constant so that it is unfolded only if the + simplified term does not expose a match in head position. 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 <substring> ..." : +- New command "Add/Remove Search Blacklist <substring> ...": 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 + The default blacklisted substrings are "_admitted" "_subproof" "Private_". - 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. @@ -141,7 +181,11 @@ Vernacular commands to avoid conversion at Qed time to go into a very long computation. - New command "Show Goal ident" to display the statement of a goal, even a closed one (available from Proof General). -- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope". +- Command "Proof" accept a new modifier "using" to force generalization + over a given list of section variables at section ending. +- New command "Arguments" generalizing "Implicit Arguments" and + "Arguments Scope" and that also allows to rename the parameters of a + definition and to tune the behavior of the tactic "simpl". Module System @@ -155,8 +199,8 @@ Module System are lower or equal than XX will be inlined. 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 Assumptions should now handle correctly opaque modules (#2168) + the flag "Set Inline Level ..." to set a level. +- Print Assumptions should now handle correctly opaque modules (#2168). - 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 @@ -166,9 +210,9 @@ Module System Libraries - Extension of the abstract part of Numbers, which now provide axiomatizations - 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. + 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. @@ -207,15 +251,15 @@ Libraries may introduce incompatibilities. In particular, the order of the arguments for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now comes first. By default, the power function now takes two BigN. -- Creation of Vector, an independant library for list indiced by their length. - Vectors' names overwrite lists' one so you shouldn't "Import" the library. - All old names change: functions' name become the CaML one and for example - Vcons become Vector.cons. You can use notations by importing +- Creation of Vector, an independent library for lists indexed by their length. + Vectors' names overwrite lists' one so you should not "Import" the library. + All old names changed: function names follow the ocaml ones and, for example, + Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing Vector.VectorNotations. - Removal of TheoryList. Requiring List instead should work most of the time. -- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and +- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and eq_rect_r (available by importing module EqNotations). -- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument) +- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument). Internal infrastructure @@ -230,8 +274,8 @@ Internal infrastructure for both make and ocamlbuild, etc. - Support of cross-compilation via mingw from unix toward Windows, contact P. Letouzey for more informations. -- new Makefile rules mli-doc to make html of mli in dev/doc/html and - full-stdlib to get a HUGE pdf with all the stdlib. +- New Makefile rules mli-doc to make html of mli in dev/doc/html and + full-stdlib to get a (huge) pdf reflecting the whole standard library. Extraction @@ -243,9 +287,8 @@ Extraction - A new command "Separate Extraction cst1 cst2 ..." that mixes a minimal extracted environment a la "Recursive Extraction" and the production of several files (one per coq source) a la "Extraction Library". - DOC TODO. - New option "Set/Unset Extraction KeepSingleton" for preventing the - extraction to optimize singleton container types. DOC TODO + extraction to optimize singleton container types. - The extraction now identifies and properly rejects a particular case of universe polymorphism it cannot handle yet (the pair (I,I) being Prop). - Support of anonymous fields in record (#2555). @@ -257,10 +300,9 @@ CoqIDE (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts, the Windows version of coqide now requires Windows >= XP SP1. -- The communication between CoqIDE and Coqtop is now done via a dialect - of XML (DOC TODO). -- The backtrack engine of CoqIDE has been reworked, it now used the - "Backtrack" command similarly to ProofGeneral. +- The communication between CoqIDE and Coqtop is now done via a dialect of XML. +- The backtrack engine of CoqIDE has been reworked, it now uses the + "Backtrack" command similarly to Proof General. - The Coqide parsing of sentences has be reworked and now supports tactic delimitation via { }. - Coqide now accepts the Abort command (wish #2357). @@ -274,15 +316,15 @@ Tools - Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, $XDG_DATA_DIRS/coq, and user-contribs before the standard library. - Coq rc file has moved to $XDG_CONFIG_HOME/coq. -- coq_makefile major cleanup. - * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work +- Major changes to coq_makefile: + * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work; * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR - with the same policy as vo in COQLIB + with the same policy as vo in COQLIB; * More variables are given by coqtop -config, others are defined only if the users doesn't have defined them elsewhere. Consequently, generated makefile - should work directly on any architecture. + should work directly on any architecture; * Packagers can take advantage of $(DSTROOT) introduction. Installation can - be made in $XDG_DATA_HOME/coq. + be made in $XDG_DATA_HOME/coq; * -arg option allows to send option as argument to coqc. Changes from V8.2 to V8.3 |