Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 122 insertions, 62 deletions

diff --git a/CHANGES b/CHANGES
index b094d8ff..5685812f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,17 +1,19 @@
-Changes from V8.0
-=================
+Changes from V8.0 to V8.1
+=========================
 
-Syntax
+Logic
 
-- 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)
+- Added sort-polymorphism on inductive families
+- Allowance for recursively non uniform parameters in inductive types
 
-Environment variables
+Syntax
 
-- 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)
+- No more support for version 7 syntax and for translation to version 8 syntax.
+- In fixpoints, the { struct ... } annotation is not mandatory any more when 
+  only one of the arguments has an inductive type (doc TODO)
+- Added disjunctive patterns in match-with patterns (doc TODO)
+- Support for primitive interpretation of string literals (doc TODO)
+- Extended support for Unicode ranges (doc TODO)
 
 Vernacular commands
 
@@ -19,101 +21,156 @@ Vernacular commands
 - 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 "Example" as synonym of "Definition" (doc TODO)
 - Added "Property", "Proposition" and "Corollary" as extra synonyms of "Lemma"
+  (doc TODO)
+- New command "Whelp" to send requests to the Helm database of proofs
+  formalized in the Calculus of Inductive Constructions (doc TODO)
+- Command "functional induction" has been re-implemented from the new
+  "definition" command.
 
-Gallina
-
-- Added disjunctive patterns in match-with patterns
-
-Ltac
+Ltac and tactic syntactic extensions
 
 - New primitive "external" for communication with tool external to Coq
-- Semantics of "match t with" changed: if a clause returns a
+  (doc TODO).
+- New semantics for "match t with": 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.
+  goal with" does) (doc TODO).
+- Hint base names can be parametric in auto and trivial.
+- Occurrence values can be parametric in unfold, pattern, etc.
+- Added entry constr_may_eval for tactic extensions.
+- Low-priority term printer made available in ML-written tactic extensions.
+- "Tactic Notation" extended to allow notations of tacticals (doc TODO).
 
 Tactics
 
 - 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.
+  with minor modifications, but deprecated).
+- When rewriting H where H is not directly a Coq equality, search first H for 
+  a registered setoid equality before starting to reduce in H. This is unlikely
+  to break any script. Should this happen nonetheless, one can insert manually 
+  some "unfold ... in H" before rewriting.
+- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
+- "rewrite ... in" now accepts a clause as place where to rewrite instead of 
+  juste a simple hypothesis name. For instance: 
+   rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
+   rewrite H in * |-  will do try rewrite H in Hi for all hypothesis Hi <> H 
+  (doc TODO).
+- Added "clear - id" to clear all hypotheses except the ones depending in id
+  (doc TODO).
 - 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
+  (it used to be a reference) (doc TODO).
+- Omega now handles arbitrary precision integers.
+- Several bug fixes in Reflexive Omega (romega).
 - 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).
+  [ foo | | bar ] stands for [ foo | idtac | bar ] (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).
+- Fixed a "fold" bug (non critical but 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
+  used to solve unresolved subterms of term arguments of tactics (doc TODO).
+- Better support for coercions to Sortclass in tactics expecting type 
+  arguments.
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
+  (doc TODO).
+- Tactic "replace" now accepts a "by" tactic clause (doc TODO).
 - 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
+  (doc TODO).
+- New introduction pattern "?" for letting Coq choose a name (doc TODO).
+- Added "eassumption" (doc TODO).
+- Added option 'using lemmas' to auto, trivial and eauto (doc TODO).
 - 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
+- Generalization 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).
+- Some small Ltac tactics has been added to the standard library 
+  (file Tactics.v):
+  * f_equal : instead of using the different f_equalX lemmas
+  * case_eq : a "case" without loss of information. An equality 
+     stating the current situation is generated in every sub-cases.
+  * swap : for a negated goal ~B and a negated hypothesis H:~A, 
+     swap H asks you to prove A from hypothesis B 
+  * revert : revert H is generalize H; clear H.
 
+Extraction
+ 
+- All type parts should now disappear instead of sometimes producing _ 
+  (for instance in Map.empty).
+- Haskell extraction: types of functions are now printed, better 
+  unsafeCoerce mechanism, both for hugs and ghc.
+- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
+- Many bug fixes.
 
 Modules
 
-- Added "Locate Module qualid" to get the full path of a module.
-- Module/Declare Module syntax made more uniform (doc TODO)
+- Added "Locate Module qualid" to get the full path of a module (TODO doc).
+- Module/Declare Module syntax made more uniform (doc TODO).
 - Added syntactic sugar "Declare Module Export/Import" and
-  "Module Export/Import" (doc TODO)
+  "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)
+   T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
 
 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.
+- Option "format" 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
+Libraries
 
-- Small extension of Zmin.V, new Zmax.v, new Zminmax.v
-- New library on String and Ascii characters (contributed by L. Thery)
+- New library on String and Ascii characters (contributed by L. Thery).
+- New library FSets+FMaps of finite sets and maps.
+- New library QArith on rational numbers.
+- Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
+- Reworking of the files on classical logic and description principles
+  (possible incompatibilities).
 - 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
+  digit 0; weaken premises in Z_lt_induction).
+- Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
+- Znumtheory now contains a gcd function that can compute within Coq.
+- More lemmas stated on Type in Wf.v, removal of redundant Fix_F.
+- Change of the internal names of lemmas in OmegaLemmas.
 - 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
+  proof scripts, set it locally opaque for compatibility).
+- More on permutations of lists in List.v and Permutation.v.
+- List.v has been much expanded.
+- New file SetoidList.v now contains results about lists seen with 
+  respect to a setoid equality.
+- Library NArith has been expanded, mostly with results coming from 
+  Intmap (for instance a bitwise xor), plus also a bridge between N and 
+  Bitvector.
+- Intmap has been reorganized. In particular its address type "addr" is 
+  now N. User contributions known to use Intmap have been adapted 
+  accordingly. If you're using this library please contact us. 
+  A wrapper FMapIntMap now presents Intmap as a particular implementation 
+  of FMaps. New developments are strongly encouraged to use either this 
+  wrapper or any other implementations of FMap instead of using directly 
+  this obsolete Intmap.
 
 Tools
 
 - 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"
+- Tool coq_makefile now removes custom targets that are file names in
+  "make clean"
+- New environment variable 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)
+
 
 Changes from V8.0beta to V8.0
 =============================
@@ -294,13 +351,16 @@ Implicit arguments
 
 Grammar extensions
 
-- UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F
-  (letter-like, including aleph and double N,Z,Q,R) are supported
-  identifiers; UTF-8 unicode blocs 2200-22FF (mathematical operators),
-  2A00-2AFF (supplemental mathematical operators) 2300-23FF
-  (miscellaneous technical, including sqrt symbol), 2600-26FF
-  (miscellaneous symbols) 2190-21FF (arrows A) and 2900-297F (arrows B)
-  are supported symbols
+- Many newly supported UTF-8 encoded unicode blocks
+  - Greek letters (0380-03FF), Hebrew letters (U05D0-05EF), letter-like
+  symbols (2100-214F, that includes double N,Z,Q,R), prime
+  signs (from 2080-2089) and characters from many written languages
+  are valid in identifiers
+  - mathematical operators (2200-22FF), supplemental mathematical
+  operators (2A00-2AFF), miscellaneous technical (2300-23FF that
+  includes sqrt symbol), miscellaneous symbols (2600-26FF), arrows
+  (2190-21FF and 2900-297F), invisible mathematical operators (from
+  2080-2089), ... are valid symbols
 
 Library