Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

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
 =============================