Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 330 insertions, 84 deletions

diff --git a/CHANGES b/CHANGES
index 4bc0bd82..ce151ee1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,49 +1,317 @@
-Changes from V8.2 to forthcoming V8.2pl1
-========================================
+Changes from V8.2 to V8.3
+=========================
 
-Language and commands
+Rewriting tactics
+
+- Tactic "rewrite" now supports rewriting on ad hoc equalities such as eq_true.
+- "Hint Rewrite" now checks that the lemma looks like an equation.
+- New tactic "etransitivity".
+- Support for heterogeneous equality (JMeq) in "injection" and "discriminate".
+- Tactic "subst" now supports heterogeneous equality and equality
+  proofs that are dependent (use "simple subst" for preserving compatibility).
+- Added support for Leibniz-rewriting of dependent hypotheses.
+- Renamed "Morphism" into "Proper" and "respect" into "proper_prf"
+  (possible source of incompatibility).
+- New tactic variants "rewrite* by" and "autorewrite*" that rewrite
+  respectively the first and all matches whose side-conditions are
+  solved.
+- "Require Import Setoid" does not export all of "Morphisms" and
+  "RelationClasses" anymore (possible source of incompatibility, fixed
+  by importing "Morphisms" too).
+- Support added for using Chung-Kil Hur's Heq library for rewriting over
+  heterogeneous equality (courtesy of the library's author).
+- Tactic "replace" supports matching terms with holes.
+
+Automation tactics
+
+- Tactic "intuition" now preserves inner "iff" and "not" (exceptional
+  source of incompatibilities solvable by redefining "intuition" as
+  "unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".)
+- Tactic "tauto" now proves classical tautologies as soon as classical logic
+  (i.e. library Classical_Prop or Classical) is loaded.
+- Tactic "gappa" has been removed from the Dp plugin.
+- Tactic "firstorder" now supports the combination of its "using" and
+  "with" options.
+- New "Hint Resolve ->" (or "<-") for declaring iff's as oriented
+  hints (wish #2104).
+- An inductive type as argument of the "using" option of "auto/eauto/firstorder"
+  is interpreted as using the collection of its constructors.
+- New decision tactic "nsatz" to prove polynomial equations 
+  by computation of Groebner bases.
+
+Other tactics
+
+- Tactic "discriminate" now performs intros before trying to discriminate an
+  hypothesis of the goal (previously it applied intro only if the goal
+  had the form t1<>t2) (exceptional source of incompatibilities - former
+  behavior can be obtained by "Unset Discriminate Introduction").
+- Tactic "quote" now supports quotation of arbitrary terms (not just the
+  goal).
+- Tactic "idtac" now displays its "list" arguments.
+- New introduction patterns "*" for introducing the next block of dependent 
+  variables and "**" for introducing all quantified variables and hypotheses.
+- Pattern Unification for existential variables activated in tactics and 
+  new option "Unset Tactic Evars Pattern Unification" to deactivate it.
+- Resolution of canonical structure is now part of the tactic's unification
+  algorithm.
+- New tactic "decide lemma with hyp" for rewriting decidability lemmas
+  when one knows which side is true.
+- Improved support of dependent goals over objects in dependent types for
+  "destruct" (rare source of incompatibility that can be avoided by unsetting
+  option "Dependent Propositions Elimination").
+- Tactic "exists", "eexists", "destruct" and "edestruct" supports iteration
+  using comma-separated arguments.
+- Tactic names "case" and "elim" now support clauses "as" and "in" and become
+  then synonymous of "destruct" and "induction" respectively.
+- A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle.
+  This tactic is simply a shortcut for "elimtype False".
+- Made quantified hypotheses get the name they would have if introduced in
+  the context (possible but rare source of incompatibilities).
+- When applying a component of a conjunctive lemma, "apply in" (and
+  sequences of "apply in") now leave the side conditions of the lemmas
+  uniformly after the main goal (possible source of rare incompatibilities).
+- In "simpl c" and "change c with d", c can be a pattern.
+- Tactic "revert" now preserves let-in's making it the exact inverse of
+  "intro".
+- New tactics "clear dependent H" and "revert dependent H" that
+  clears (resp. reverts) H and all the hypotheses that depend on H.
+- Ltac's pattern-matching now supports matching metavariables that
+  depend on variables bound upwards in the pattern.
 
-- Fixing Not_found bug in Theorem with.
-- Fixing pattern parsing bug #2087.
-- Fixing name aliases bug #2085 with modules.
-- Fixing checker bug #2065 with -impredicative-set option.
-- Complying with 8.1 heuristic when unification returns several solutions.
-- Add [Print Opaque Dependencies] command to print the assumptions and 
-  the opaque constants a definition uses.
-- Fixing performance issue in Program's type inference when there are
-  many existentials.
-- Fixing bug #2093, using Program does not require to import Program.Tactics
-  anymore, it will use [idtac] as the default obligation tactic.
-- Fix imports when requiring Setoid, to avoid cluttering the context with
-  internal names (possible source of incompatibility, import Morphisms to fix).
-- Fixing bug #2089, Combined Scheme was not treating parameters correctly.
-- Fixing Program to use hooks correctly, when called through [Program Coercion]
-  for example.
-- Fixing manual implicit arguments to always work and remove 
-  [Set Manual Implicit Arguments] option (possible source of incompatibility).
-- Fixing refine to work with typeclasses.
-- Fixing implementation of [Context] to discharge class instances only on definitions
-  using some of the parameters or the instance itself (possible source of 
-  incompatibility).
+Tactic definitions
 
-Tactics
+- Ltac definitions support Local option for non-export outside modules.
+- Support for parsing non-empty lists with separators in tactic notations.
+- New command "Locate Ltac" to get the full name of an Ltac definition.
+
+Notations
+
+- Record syntax "{|x=...; y=...|}" now works inside patterns too.
+- Abbreviations from non-imported module now invisible at printing time.
+- Abbreviations now use implicit arguments and arguments scopes for printing.
+- Abbreviations to pure names now strictly behave like the name they refer to
+  (make redirections of qualified names easier).
+- Abbreviations for applied constant now propagate the implicit arguments
+  and arguments scope of the underlying reference (possible source of
+  incompatibilities generally solvable by changing such abbreviations from
+  e.g. "Notation foo' := (foo x)" to "Notation foo' y := (foo x (y:=y))").
+- The "where" clause now supports multiple notations per defined object.
+- Recursive notations automatically expand one step on the left for better
+  factorization; recursion notations inner separators now ensured being tokens.
+- Added "Reserved Infix" as a specific shortcut of the corresponding
+  "Reserved Notation".
+- Open/Close Scope command supports Global option in sections.
+
+Specification language
+
+- New support for local binders in the syntax of Record/Structure fields.
+- Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
+- Binders given before ":" in lemmas and in definitions built by tactics are
+  now automatically introduced (possible source of incompatibility that can
+  be resolved by invoking "Unset Automatic Introduction").
+
+Module system
+
+- Include Type is now deprecated since Include now accept both modules and
+  module types.
+- Declare ML Module supports Local option.
+- The sharing between non-logical object and the management of the
+  name-space has been improved by the new "Delta-equivalence" on
+  qualified name.
+- The include operator has been extended to high-order structures
+- Sequences of Include can be abbreviated via new syntax "<+".
+- A module (or module type) can be given several "<:" signatures.
+- Interactive proofs are now permitted in module type. Functors can hence
+  be declared as Module Type and be used later to type themselves.
+- A functor application can be prefixed by a "!" to make it ignore any
+  "Inline" annotation in the type of its argument(s) (for examples of
+  use of the new features, see libraries Structures and Numbers).
+
+Extraction
+
+- When using (Recursive) Extraction Library, the filenames are directly the
+  Coq ones with new appropriate extensions : we do not force anymore
+  uncapital first letters for Ocaml and capital ones for Haskell.
+- The extraction now tries harder to avoid code transformations that can be
+  dangerous for the complexity. In particular many eta-expansions at the top
+  of functions body are now avoided, clever partial applications will likely
+  be preserved, let-ins are almost always kept, etc.
+- Harsh support of module extraction to Haskell and Scheme: module hierarchy
+  is flattened, module abbreviations and functor applications are expanded,
+  module types and unapplied functors are discarded.
+- Less unsupported situations when extracting modules to Ocaml. In particular
+  module parameters might be alpha-renamed if a name clash is detected.  
+- Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
+- Extraction Implicit: this new experimental command allows to mark
+  some arguments of a function or constructor for removed during
+  extraction, even if these arguments don't fit the usual elimination
+  principles of extraction, for instance the length n of a vector.
+- Files ExtrOcaml*.v in plugins/extraction try to provide a library of common
+  extraction commands: mapping of basics types toward Ocaml's counterparts,
+  conversions from/to int and big_int, or even complete mapping of nat,Z,N
+  to int or big_int, or mapping of ascii to char and string to char list
+  (in this case recognition of ascii constants is hard-wired in the extraction).
 
-- Fixing correct binding of quantified hypotheses for induction/destruction
-  when used in Ltac.
-- Fixing bad parentheses check in "pose (f binders := ...)" syntax.
-- Fixing unbalanced parenthesis in Ltac debug trace printer.
-- Fixing missing sort unification check in lemma application (bug #2084).
-- Fixing "as" clause of "apply in" that was not working in the general case.
-- Fixing eauto not using external hints with no pattern.
+Program
+
+- Streamlined definitions using well-founded recursion and measures so
+  that they can work on any subset of the arguments directly (uses currying).
+- Try to automatically clear structural fixpoint prototypes in
+  obligations to avoid issues with opacity.
+- Use return type clause inference in pattern-matching as in the standard 
+  typing algorithm.
+- Support [Local Obligation Tactic] and [Next Obligation with tactic].
+- Use [Show Obligation Tactic] to print the current default tactic.
+- [fst] and [snd] have maximal implicit arguments in Program now (possible 
+  source of incompatibility).
+
+Type classes
+
+- Declaring axiomatic type class instances in Module Type should be now
+  done via new command "Declare Instance", while the syntax "Instance"
+  now always provides a concrete instance, both in and out of Module Type.
+- Use [Existing Class foo] to declare foo as a class a posteriori.
+  [foo] can be an inductive type or a constant definition. No
+  projections or instances are defined.
+- Various bug fixes and improvements: support for defined fields, 
+  anonymous instances, declarations giving terms, better handling of
+  sections and [Context].
+
+Vernacular commands
 
-Tools and development
+- New command "Timeout <n> <command>." interprets a command and a timeout
+  interrupts the interpretation after <n> seconds.
+- New command "Compute <expr>." is a shortcut for "Eval vm_compute in <expr>".
+- New command "Fail <command>." interprets a command and is successful iff
+  the command fails on an error (but not an anomaly). Handy for tests and
+  illustration of wrong commands.
+- Most commands referring to constant (e.g. Print or About) now support
+  referring to the constant by a notation string.
+- Made generation of boolean equality automatic for datatypes (use
+  "Unset Boolean Equality Schemes" for deactivation).
+- Made support for automatic generation of case analysis schemes and
+  congruence schemes available to user (governed by options "Unset
+  Case Analysis Schemes" and "Unset Congruence Schemes").
+- New command "(Global?) Generalizable [All|No] Variable(s)? ident(s)?" to
+  declare which identifiers are generalizable in `{} and `() binders.
+- New command "Print Opaque Dependencies" to display opaque constants in
+  addition to all variables, parameters or axioms a theorem or
+  definition relies on.
+- New command "Declare Reduction <id> := <conv_expr>", allowing to write
+  later "Eval <id> in ...". This command accepts a Local variant.
+- Syntax of Implicit Type now supports more than one block of variables of
+  a given type.
+- Command "Canonical Structure" now warns when it has no effects.
 
-- Fixing missing -c option in coq_makefile.
-- Temporary hack for coqide.byte "double free or corruption" problem.
-- Added support for code development under Bazaar.
-- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
-- Parsing fixes and support for parsing regular comments inline in coqdoc,
-  using option -parse-comments (suggestions by B. Pierce).
+Library
+
+- Use "standard" Coq names for the properties of eq and identity
+  (e.g. refl_equal is now eq_refl). Support for compatibility is provided.
+- The function Compare_dec.nat_compare is now defined directly,
+  instead of relying on lt_eq_lt_dec. The earlier version is still
+  available under the name nat_compare_alt.
+- Lemmas in library Relations and Reals have been homogenized a bit.
+- The implicit argument of Logic.eq is now maximally inserted, allowing
+  to simply write "eq" instead of "@eq _" in morphism signatures.
+- Wrongly named lemmas (Zlt_gt_succ and Zlt_succ_gt) fixed (potential source
+  of incompatibilities)
+- List library:
+  - Definitions of list, length and app are now in Init/Datatypes.
+    Support for compatibility is provided.
+  - Definition of Permutation is now in Sorting/Permtation.v
+  - Some other light revisions and extensions (possible source
+    of incompatibilities solvable by qualifying names accordingly).
+- In ListSet, set_map has been fixed (source of incompatibilities if used).
+- Sorting library:
+  - new mergesort of worst-case complexity O(n*ln(n)) made available in 
+    Mergesort.v;
+  - former notion of permutation up to setoid from Permutation.v is
+    deprecated and moved to PermutSetoid.v;
+  - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated;
+  - new file Sorted.v for some definitions of being sorted.
+- Structure library. This new library is meant to contain generic
+  structures such as types with equalities or orders, either
+  in Module version (for now) or Type Classes (still to do):
+  - DecidableType.v and OrderedType.v: initial notions for FSets/FMaps,
+    left for compatibility but considered as deprecated.
+  - Equalities.v and Orders.v: evolutions of the previous files,
+    with fine-grain Module architecture, many variants, use of
+    Equivalence and other relevant Type Classes notions.
+  - OrdersTac.v: a generic tactic for solving chains of (in)equalities
+    over variables. See {Nat,N,Z,P}OrderedType.v for concrete instances.
+  - GenericMinMax.v: any ordered type can be equipped with min and max.
+    We derived here all the generic properties of these functions.
+- MSets library: an important evolution of the FSets library.
+  "MSets" stands for Modular (Finite) Sets, by contrast with a forthcoming
+  library of Class (Finite) Sets contributed by S. Lescuyer which will be
+  integrated with the next release of Coq. The main features of MSets are:
+  - The use of Equivalence, Proper and other Type Classes features
+    easing the handling of setoid equalities.
+  - The interfaces are now stated in iff-style. Old specifications
+    are now derived properties.
+  - The compare functions are now pure, and return a "comparison" value.
+    Thanks to the CompSpec inductive type, reasoning on them remains easy.
+  - Sets structures requiring invariants (i.e. sorted lists) are
+    built first as "Raw" sets (pure objects and separate proofs) and
+    attached with their proofs thanks to a generic functor. "Raw" sets
+    have now a proper interface and can be manipulated directly.
+  Note: No Maps yet in MSets. The FSets library is still provided
+  for compatibility, but will probably be considered as deprecated in the
+  next release of Coq.
+- Numbers library:
+  - The abstract layer (NatInt, Natural/Abstract, Integer/Abstract) has
+    been simplified and enhance thanks to new features of the module
+    system such as Include (see above). It has been extended to Euclidean
+    division (three flavors for integers: Trunc, Floor and Math).
+  - The arbitrary-large efficient numbers (BigN, BigZ, BigQ) has also
+    been reworked. They benefit from the abstract layer improvements
+    (especially for div and mod). Note that some specifications have
+    slightly changed (compare, div, mod, shift{r,l}). Ring/Field should
+    work better (true recognition of constants).
+
+Tools
+
+- Option -R now supports binding Coq root read-only.
+- New coqtop/coqc option -beautify to reformat .v files (usable
+  e.g. to globally update notations).
+- New tool beautify-archive to beautify a full archive of developments.
+- New coqtop/coqc option -compat X.Y to simulate the general behavior
+  of previous versions of Coq (provides e.g. support for 8.2 compatibility).
+
+Coqdoc
+
+- List have been revamped.  List depth and scope is now determined by
+  an "offside" whitespace rule.
+- Text may be italicized by placing it in _underscores_.
+- The "--index <string>" flag changes the filename of the index.
+- The "--toc-depth <int>" flag limits the depth of headers which are
+  included in the table of contents.
+- The "--lib-name <string>" flag prints "<string> Foo" instead of
+  "Library Foo" where library titles are called for.  The
+  "--no-lib-name" flag eliminates the extra title.
+- New option "--parse-comments" to allow parsing of regular "(* *)"
+  comments.
+- New option "--plain-comments" to disable interpretation inside comments.
+- New option "--interpolate" to try and typeset identifiers in Coq escapings
+  using the available globalization information.
+- New option "--external url root" to refer to external libraries.
+- Links to section variables and notations now supported.
+
+Internal infrastructure
+
+- To avoid confusion with the repository of user's contributions,
+  the subdirectory "contrib" has been renamed into "plugins".
+  On platforms supporting ocaml native dynlink, code located there
+  is built as loadable plugins for coqtop.
+- An experimental build mechanism via ocamlbuild is provided.
+  From the top of the archive, run ./configure as usual, and
+  then ./build. Feedback about this build mechanism is most welcome.
+  Compiling Coq on platforms such as Windows might be simpler
+  this way, but this remains to be tested.
+- The Makefile system has been simplified and factorized with
+  the ocamlbuild system. In particular "make" takes advantage
+  of .mllib files for building .cma/.cmxa. The .vo files to
+  compile are now listed in several vo.itarget files.
 
 Changes from V8.1 to V8.2
 =========================
@@ -60,7 +328,6 @@ Language
   arguments in terms.
 - Sort of Record/Structure, Inductive and CoInductive defaults to Type
   if omitted.
-- Support for optional "where" notation clauses for record fields.
 - (Co)Inductive types can be defined as records 
   (e.g. "CoInductive stream := { hd : nat; tl : stream }.")
 - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
@@ -75,10 +342,6 @@ Language
   As a consequence, Acc_rect has now a more direct proof [possible source
   of easily fixed incompatibility in case of manual definition of a recursor
   in a recursive singleton inductive type].
-- New syntax to do implicit generalization in binders and inside terms.
-- New tentative syntax for introduction of record objects without mentioning 
-  the constructor {| field := body; ... |}, turning missing fields into holes
-  (compatible with refine and Program).
 
 Vernacular commands
 
@@ -117,14 +380,6 @@ Vernacular commands
 - "Declare ML Module" now allows to import .cmxs files when Coq is
   compiled in native code with a version of OCaml that supports native
   Dynlink (>= 3.11).
-- New command "Create HintDb name [discriminated]" to explicitely declare
-  a new hint database and optionaly turn on a discrimination net 
-  implementation to index all the lemmas in the database.
-- New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
-  status of definitions used by auto. This information is taken into account
-  by the discrimination net and the unification algorithm.
-- "Hint Extern" now takes an optional pattern and applies the given tactic
-  all the time if no pattern is given.
 - Specific sort constraints on Record now taken into account.
 - "Print LoadPath" supports a path argument to filter the display.
 
@@ -231,6 +486,7 @@ Libraries
   contribution repository (contribution CoC_History). New lemmas about 
   transitive closure added and some bound variables renamed (exceptional
   risk of incompatibilities).
+- Syntax for binders in terms (e.g. for "exists") supports anonymous names.
 
 Notations, coercions, implicit arguments and type inference
 
@@ -238,13 +494,13 @@ Notations, coercions, implicit arguments and type inference
   pattern-matching problems.
 - Experimental allowance for omission of the clauses easily detectable as
   impossible in pattern-matching problems.
-- Improved inference of implicit arguments, now working inside record
-  declarations.
+- Improved inference of implicit arguments.
 - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
   Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
   Defensive" for controlling inference and use of implicit arguments.
 - New modifier in "Implicit Arguments" to force an implicit argument to
   be maximally inserted.
+- New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
 - New options Global and Local to "Implicit Arguments" for section
   surviving or non export outside module.
 - Level "constr" moved from 9 to 8.
@@ -260,8 +516,6 @@ Tactic Language
   (syntax for second-order unification variable is "@?X").
 - Support for matching on let bindings in match context using syntax
   "H := body" or "H := body : type".
-- (?X ?Y) patterns now match any application instead of only unary 
-  applications (possible source of incompatibility).
 - Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
 - The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
   is extended so that at most one expr_i may have the form "expr .."
@@ -286,15 +540,11 @@ Tactic Language
   metavariable in "match" and it gets instantiated by an identifier
   (allow e.g. to extract the name of a statement like "exists x, P x").
 - New printing of Ltac call trace for better debugging.
-- The C-zar (formerly know as declarative) proof language is now properly
-  documented. 
 
 Tactics
 
 - New tactics "apply -> term", "apply <- term", "apply -> term in
   ident", "apply <- term in ident" for applying equivalences (iff).
-- "apply" and "rewrite" now take open terms (terms with undefined existentials) 
-  as input.
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
 - New tactics "eapply in", "erewrite", "erewrite in".
@@ -389,6 +639,9 @@ Program
   programming (id, apply, flip...)
 - More robust obligation handling, dependent pattern-matching and
   well-founded definitions.
+- New syntax " dest term as pat in term " for destructing objects using
+  an irrefutable pattern while keeping equalities (use this instead of 
+  "let" in Programs).
 - Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer 
   which argument decreases structurally.
 - Program Lemma, Axiom etc... now permit to have obligations in the statement 
@@ -407,8 +660,8 @@ Type Classes
 
 - New "Class", "Instance" and "Program Instance" commands to define
   classes and instances documented in the reference manual.  
-- New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}" 
-  for binding type classes, usable everywhere.
+- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " 
+  for binding type classes, usable everywhere.  
 - New command " Print Classes " and " Print Instances some_class " to
   print tables for typeclasses.  
 - New default eauto hint database "typeclass_instances" used by the default
@@ -432,9 +685,10 @@ Setoid rewriting
   Their introduction may break existing scripts that defined 
   them as notations with different levels.
   
-  - One can use [Typeclasses Opaque/Transparent [cst]] to indicate
-  that [cst] should not be unfolded during unification for morphism
-  resolution, by default all constants are transparent.
+  - One needs to use [Typeclasses unfold [cst]] if [cst] is used
+  as an abbreviation hiding products in types of morphisms,
+  e.g. if ones redefines [relation] and declares morphisms 
+  whose type mentions [relation].
 
   - The [setoid_rewrite]'s semantics change when rewriting with
   a lemma: it can rewrite two different instantiations of the lemma
@@ -454,12 +708,12 @@ Setoid rewriting
   new [Add Parametric] commands, documented in the manual.
 
   - Setoid_Theory is now an alias to Equivalence, scripts building objects
-  of type Setoid_Theory need to unfold (or [red]) the definitions
+  of type Setoid_Theory need to unfold (or "red") the definitions
   of Reflexive, Symmetric and Transitive in order to get the same goals 
   as before. Scripts which introduced variables explicitely will not break.
 
   - The order of subgoals when doing [setoid_rewrite] with side-conditions
-  is now always the same: first the new goal, then the conditions.
+  is always the same: first the new goal, then the conditions.
 
 - New standard library modules Classes.Morphisms declares
   standard morphisms on refl/sym/trans relations.
@@ -512,19 +766,11 @@ Tools
 - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
 - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
 - The binary "parser" has been renamed to "coq-parser".
-
-coqdoc
 - Improved coqdoc and dump of globalization information to give more 
   meta-information on identifiers. All categories of Coq definitions are 
-  supported, which makes typesetting trivial in the generated documentation. 
-- A "--interpolate" option permits to use typesetting information from the 
-  typechecked part of the file to typeset identifiers appearing in Coq escapings
-  inside the documentation. 
-- Better handling of utf8 ("--utf8" option) and respect of spaces in the source.
-- Support for hyperlinking and indexing developments in the TeX output.
-- New option "color" of the coqdoc style file to render identifiers using colors.
-- Additional macros in the TeX ouput allowing to customize indentation and size of
-  empty lines. New environment "coqdoccode" for Coq code.
+  supported, which makes typesetting trivial in the generated documentation.
+  Support for hyperlinking and indexing developments in the tex output
+  has been implemented as well.
 
 Miscellaneous
 
@@ -1061,7 +1307,7 @@ Tactics
 - Clear now fails when trying to remove a local definition used by
   a constant appearing in the current goal
 
-Extraction (See details in contrib/extraction/CHANGES)
+Extraction (See details in plugins/extraction/CHANGES)
 
 - The old commands: 	(Recursive) Extraction Module M.
   are now:              (Recursive) Extraction Library M. 
@@ -1201,7 +1447,7 @@ Tactics
 - Unfold expects a correct evaluable argument
 - Clear expects existing hypotheses
 
-Extraction (See details in contrib/extraction/CHANGES and README):
+Extraction (See details in plugins/extraction/CHANGES and README):
 
 - An experimental Scheme extraction is provided.
 - Concerning Ocaml, extracted code is now ensured to always type-check, 
@@ -1316,7 +1562,7 @@ Bugs
 - Known bugs related to Inversion and let-in's fixed
 - Bug unexpected Delta with let-in now fixed
 
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
 
 - Signatures of extracted terms are now mostly expunged from dummy arguments.
 - Haskell extraction is now operational (tested & debugged).  
@@ -1324,7 +1570,7 @@ Extraction (details in contrib/extraction/CHANGES or documentation)
 Standard library
 
 - Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
-  and Zlogarithms.v) moved from contrib/omega in order to be more
+  and Zlogarithms.v) moved from plugins/omega in order to be more
   visible, one Zsgn function, more induction principles (Wf_Z.v and
   tail of Zcomplements.v), one more general Euclid theorem
 - Peano_dec.v and Compare_dec.v now part of Arith.v
@@ -1387,7 +1633,7 @@ Tactics
 - Slight improvement in naming strategy for NewInduction/NewDestruct
 - Intuition/Tauto do not perform useless unfolding and work up to conversion
 
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
 
 - Syntax changes: there are no more options inside the extraction commands. 
   New commands for customization and options have been introduced instead.