summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /CHANGES
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES157
1 files changed, 99 insertions, 58 deletions
diff --git a/CHANGES b/CHANGES
index 7c7f5dc7..b094d8ff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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
=============================