diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 157 |
1 files changed, 99 insertions, 58 deletions
@@ -1,78 +1,119 @@ -Changes from V8.0pl2 to V8.0pl3 -=============================== +Changes from V8.0 +================= -Tactics +Syntax -- The search depth argument of auto can be parameterised in the - Ltac language -- Added entry constr_may_eval for tactic extensions (new syntax) +- No more support for version 7 syntax and for translation to version 8 syntax. +- Support for primitive interpretation of string literals +- Extended support for Unicode ranges (Unicode doc TODO) -Compilation +Environment variables -- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0. +- COQREMOTEBROWSER to set the command invoked to start the remote browser + both in Coq and coqide. Standard syntax: "%s" is the placeholder for the + URL (doc TODO) -Standard library +Vernacular commands -- A couple of lemmas of ZArith were renamed. This concerns names - containing O (the letter), which is replaced by 0 (the number). +- Added "Print Ltac qualid" to print a user defined tactic (doc TODO) +- Added "Print Rewrite HintDb" to print the content of a DB used by + autorewrite (doc TODO) +- Added "Print Canonical Projections" (doc TODO) +- Added "Example" as synonym of "Definition" +- Added "Property", "Proposition" and "Corollary" as extra synonyms of "Lemma" -Bug fixes +Gallina -- Fixes a serious bug in CoqIde. The windows port should be able - to load large libraries (such as Reals) without producing the - "bad file descriptor" error. -- Scope of Ltac variables: global Ltac macros no longer hide goal - hypotheses -- Many fixes concerning extraction: - * fewer useless eta-expansions - * for Ocaml: extraction of records should be ok now. Problem with - type t = M.t in modules fixed. - * in Haskell: improved use of unsafeCoerce, fixed Extract Constant, - function types are now printed. - * important revision of the Scheme extraction: - see http://www.pps.jussieu.fr/~letouzey/scheme -- Fixes a bug in the interpretation of record projections ("bad number - of parameters" error) -- Fixed a bug in the omega tactic -- Fixed a bug in the fold tactic regarding hypotheses ordering -- Pretty-print of universes fixed -- Added an empty level 99 in patterns syntax entry -- "Notation" bug fixes ("only parsing" bug, printing of numerals - arguments of coercions, default spacing for recursive notations - with no terminal separator, "Tactic Notation" printer). - -Changes from V8.0pl1 to V8.0pl2 -=============================== +- Added disjunctive patterns in match-with patterns -Notations +Ltac -- Option "format" now aware of recursive notations +- New primitive "external" for communication with tool external to Coq +- Semantics of "match t with" changed: if a clause returns a + tactic, it is now applied to the current goal. If it fails, the next + clause or next matching subterm is tried (i.e. it behaves as "match + goal with"). +- New modifier "lazy" (TODO) for "match t with" and "match goal with" telling + to delay the evaluation of tactic expression. +- Hint base name can be parametric in auto and trivial. -Bug fixes +Tactics -- Tactic "fail n" for n<>0 now works (notice that each "match term with" - block decreases the failure level, in accordance with the intuition but - not in conformity with the reference manual) -- Option -dump-glob now strips module segment as expected by coqdoc (which - is still not aware of modules) -- See coq-bugs web page for a full list of fixed bugs (look for - fixes committed before Jan 2005 to cvs version V8-0-bugfix) +- New implementation and generalization of [setoid_]* (setoid_rewrite, + setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite). + New syntax for declaring relations and morphisms (old syntax still working + with minor modifications, but deprecated) (doc TODO) +- Added "clear - id" to clear all hypotheses except the ones depending in id. +- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO) +- The argument of Declare Left Step and Declare Right Step is now a term + (it used to be a reference) (doc TODO) +- Omega now handles arbitrary precision integers +- Idtac can now be left implicit in a [...|...] construct: for instance, + [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). +- "Tactic Notation" extended to allow notations of tacticals (doc TODO). +- Added "autorewrite with ... in hyp [using ...]" (doc TODO). +- Added entry constr_may_eval for tactic extensions (new syntax). +- Fixed a "fold" bug (non critical and possible source of incompatibilities). +- Added classical_left and classical_right which transforms |- A \/ B into + ~B |- A and ~A |- B respectively. +- Added command "Declare Implicit Tactic" to set up a default tactic to be + used to solve unresolved subterms of term arguments of tactics. +- Better support for coercions to Sortclass in tactics expecting type arguments +- Low-priority term printer made available in ML-written tactic extensions +- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses +- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns +- New introduction pattern "?" for letting Coq choose a name +- Added "eassumption" +- Added option 'using lemmas' to auto, trivial and eauto +- Numbering of "pattern", "unfold", "simpl", ... occurrences in "match + with" made consistent with the printing of the return clause after + the term to match in the "match-with" construct (use "Set Printing All" + to see hidden occurrences). +- New definition command: "GenFixpoint" (TODO) (doc) +- functional induction has been re-implemented from the new definition + command (doc TODO) +- Genralisation of induction "induction x1...xn using scheme" where + scheme is an induction principle with complex predicates (like the + ones generated by function induction) (doc TODO). -Changes from V8.0 to V8.0pl1 -============================ -Unicode support +Modules -- Miscellaneous Mathematical Symbols-A and B, and Supplemental - Arrows-A now supported +- Added "Locate Module qualid" to get the full path of a module. +- Module/Declare Module syntax made more uniform (doc TODO) +- Added syntactic sugar "Declare Module Export/Import" and + "Module Export/Import" (doc TODO) +- Added syntactic sugar "Module M(Export/Import X Y: T)" and + "Module Type M(Export/Import X Y: T)" + (only for interactive definitions) (doc TODO) +- Construct "with" generalized to module paths: + T with (Definition|Module) M1.M2....Mn.l := l'. (doc TODO) -Bug fixes +Notations + +- "format" option aware of recursive notations. +- added insertion of spaces by default in recursive notations w/o separators. +- no more automatic printing box in case of user-provided printing "format". +- new notation "exists! x:A, P" for unique existence. + +Library + +- Small extension of Zmin.V, new Zmax.v, new Zminmax.v +- New library on String and Ascii characters (contributed by L. Thery) +- Few other improvements in ZArith potentially exceptionally breaking the + compatibility (useless hypothesys of Zgt_square_simpl and + Zlt_square_simpl removed; fixed names mentioning letter O instead of + digit 0; weaken premises in Z_lt_induction) +- More lemmas stated on Type in Wf.v, removal of redundant Fix_F +- Coq.List.In_dec has been set transparent (this may exceptionally break + proof scripts, set it locally opaque for compatibility) +- Change of the internal names of lemmas in OmegaLemmas + +Tools -- GPL-incompatible QPL files for CoqIde are now GPL -- Pretty-printing of coercions to Funclass fixed and improved -- Erroneous interpretation of the quantified hypothesis in intro until fixed -- See coq-bugs web page for a full list of fixed bugs (look for - fixes in V8-0-bugfix before July 17) +- New semantics for coqtop options ("-batch" expects option "-top dir" + for loading vernac file that contains definitions). +- coq_makefile now removes custom targets that are file names in "make clean" Changes from V8.0beta to V8.0 ============================= |