Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

6 files changed, 551 insertions, 11 deletions

diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
new file mode 100644
index 00000000..c825f088
--- /dev/null
+++ b/dev/doc/build-system.dev.txt
@@ -0,0 +1,70 @@
+Since July 2007, Coq features a build system overhauled by Pierre
+Corbineau and Lionel Elie Mamane.
+
+This file documents internals of the implementation of the build
+system. For what a Coq developer needs to know about the build system,
+see build-system.txt .
+
+.ml4 files
+----------
+
+.ml files corresponding to .ml4 files are created to keep ocamldep
+happy only. To ensure they are not used for compilation, they contain
+invalid OCaml.
+
+multi-stage build
+-----------------
+
+Le processus de construction est séparé en trois étapes qui correspondent
+aux outils nécessaires pour calculer les dépendances de cette étape:
+
+stage1: ocamldep, sed , camlp4 sans fichiers de Coq
+stage2: camlp4 avec grammar.cma et/ou q_constr.cmo
+stage3: coqdep (.vo)
+
+Le Makefile a été séparé en plusieurs fichiers :
+
+- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf
+  clean et les fichiers pour emacs (car ils sont en quelque sorte en
+  "stage0": aucun calcul de dépendance nécessaire).
+- Makefile.common : définitions des variables (essentiellement des
+  listes de fichiers)
+- Makefile.build : les règles de compilation sans inclure de
+  dépendances
+- Makefile.stage* : fichiers qui incluent les dépendances calculables
+  à cette étape ainsi que Makefile.build.
+
+The build needs to be cut in stages because make will not take into
+account one include when making another include.
+
+Parallélisation
+---------------
+
+Le découpage en étapes veut dire que le makefile est un petit peu
+moins parallélisable que strictement possible en théorie: par exemple,
+certaines choses faites en stage2 pourraient être faites en parallèle
+avec des choses de stage1. Nous essayons de minimiser cet effet, mais
+nous ne l'avons pas complètement éliminé parce que cela mènerait à un
+makefile très complexe. La minimisation est principalement que si on
+demande un objet spécifique (par exemple "make parsing/g_constr.cmx"),
+il est fait dans l'étape la plus basse possible (simplement), mais si
+un objet est fait comme dépendance de la cible demandée (par exemple
+dans un "make world"), il est fait le plus tard possible (par exemple,
+tout code OCaml non nécessaire pour coqdep ni grammar.cma ni
+q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet
+le parallélisme de compilation de code OCaml et de fichiers Coq (.v)).
+
+Le "(simplement)" ci-dessus veut dire que savoir si un fichier non
+nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en
+stage1 est compliqué avec make, alors nous retombons en général sur le
+stage2. La séparation entre le stage2 et stage3 est plus facile, donc
+l'optimisation ci-dessus s'y applique pleinement.
+
+En d'autres mots, nous avons au niveau conceptuel deux assignations
+d'étape pour chaque fichier:
+
+ - l'étape la plus petite où nous savons qu'il peut être fait.
+ - l'étape la plus grande où il peut être fait.
+
+Mais seule la première est gérée explicitement, la seconde est
+implicite.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
new file mode 100644
index 00000000..c9571f7c
--- /dev/null
+++ b/dev/doc/build-system.txt
@@ -0,0 +1,299 @@
+Since July 2007, Coq features a build system overhauled by Pierre
+Corbineau and Lionel Elie Mamane.
+
+This file documents what a Coq developer needs to know about the build
+system. If you want to enhance the build system itself (or are curious
+about its implementation details), see build-system.dev.txt .
+
+The build system is not at its optimal state, see TODO section.
+
+Stages in build system
+----------------------
+
+The build system is separated into three stages, corresponding to the
+tool(s) necessary to compute the dependencies necessary at this stage:
+
+stage1: ocamldep, sed, camlp4 without Coq extensions
+stage2: camlp4 with grammar.cma and/or q_constr.cmo
+stage3: coqdep (.vo)
+
+The file "Makefile" itself serves as minimum stage for targets that
+should not need any dependency (such as *clean*).
+
+Changes (for old-timers)
+------------------------
+
+The contents of the old Makefile has been mostly split into:
+
+ - variable declarations for file lists in Makefile.common.
+
+   These declarations are now static (for faster Makefile execution),
+   so their definitions are order-dependent.
+
+ - actual building rules and compiler flags variables in
+   Makefile.build
+
+
+The handling of globals is now: the globals of FOO.v are in FOO.glob
+and the global glob.dump is created by concatenation of all .glob
+files. In particular, .glob files are now always created.
+
+See also section "cleaning targets"
+
+Reducing build system overhead
+------------------------------
+
+When you are actively working on a file in a "make a change, make to
+test, make a change, make to test", etc mode, here are a few tips to
+save precious time:
+
+ - Always ask for what you want directly (e.g. bin/coqtop,
+   foo/bar.cmo, ...), don't do "make world" and interrupt
+   it when it has done what you want. This will try to minimise the
+   stage at which what you ask for is done (instead of maximising it
+   in order to maximise parallelism of the build process).
+
+   For example, if you only want to test whether bin/coqtop still
+   builds (and eventually start it to test your bugfix or new
+   feature), don't do "make world" and interrupt it when bin/coqtop is
+   built. Use "make bin/coqtop" or "make coqbinaries" or something
+   like that. This will avoid entering the stage 3, and cut build
+   system overhead by 50% (1.2s instead of 2.4 on writer's machine).
+
+ - You can turn off rebuilding of the standard library each time
+   bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1.
+
+ - If you want to avoid all .ml4 files being recompiled only because
+   grammar.cma was rebuilt, do "make ml4depclean" once and then use
+   NO_RECOMPILE_ML4=1.
+
+ - The CM_STAGE1=1 option to make will build all .cm* files mentioned
+   as targets on the command line in stage1. Whether this will work is
+   your responsibility. It should work for .ml files that don't depend
+   (nor directly nor indirectly through transitive closure of the
+   dependencies) on any .ml4 file, or where those dependencies can be
+   safely ignored in the current situation (e.g. all these .ml4 files
+   don't need to be recompiled).
+
+   This will avoid entering the stage2 (a reduction of 33% in
+   overhead, 0.4s on the writer's machine).
+
+ - To jump directly into a stage (e.g. because you know nothing is to
+   be done in stage 1 or (1 and 2) or because you know that the target
+   you give can be, in this situation, done in a lower stage than the
+   build system dares to), use GOTO_STAGE=n. This will jump into stage
+   n and try to do the targets you gave in that stage.
+
+ - To disable all dependency recalculation, use the NO_RECALC_DEPS=1
+   option. It disables REcalculation of dependencies, not calculation
+   of dependencies. In other words, if a .d file does not exist, it is
+   still created, but it is not updated every time the source file
+   (e.g. .ml) is changed.
+
+General speed improvements:
+
+ - When building both the native and bytecode versions, the
+   KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
+   by running camlp4o only once on every .ml4 file, at the expense of
+   readability of compilation error messages for .ml4 files.
+
+Dependencies
+------------
+
+There are no dependencies in the archive anymore, they are always
+bootstrapped. The dependencies of a file FOO are in FOO.d . This
+enables partial recalculation of dependencies (only the dependencies
+of changed files are recomputed).
+
+If you add a dependency to a Coq camlp4 extension (grammar.cma or
+q_constr.cmo), then see sections ".ml4 files" and "new files".
+
+Cleaning Targets
+----------------
+
+Targets for cleaning various parts:
+
+ - distclean: clean everything; must leave only what should end up in
+   distribution tarball and/or is in a svn checkout.
+
+ - clean: clean everything except effect of "./configure" and documentation.
+
+ - cleanconfig: clean effect of "./configure" only
+
+ - archclean:  remove all architecture-dependent   generated files
+ - indepclean: remove all architecture-independent generated files
+   (not documentation)
+
+ - objclean: clean all generated files, but not Makefile meta-data
+   (e.g. dependencies), nor debugging/development information nor
+   other cruft (e.g. editor backup files), nor documentation
+
+ - docclean: clean documentation
+
+.ml4 files
+----------
+
+The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
+can be obtained with:
+ make FOO.ml4-preprocessed
+
+If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
+or q_constr.cmo), it must contain a line like:
+ (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
+
+If it uses a standard grammar extension, it must contain a line like:
+ (*i camlp4use: "pa_ifdef.cmo" i*)
+
+It can naturally contain both a camlp4deps and a camlp4use line. Both
+are used for preprocessing. It is thus _not_ necessary to add a
+specific rule for a .ml4 file in the Makefile.build just because it
+uses grammar extensions.
+
+By default, the build system is geared towards development that may
+use the Coq grammar extensions, but not development of Coq's grammar
+extensions themselves. This means that .ml4 files are compiled
+directly (using ocamlc/opt's -pp option), without use of an
+intermediary .ml (or .ml4-preprocessed) file. This is so that if a
+compilation error occurs, the location in the error message is a
+location in the .ml4 file. If you are modifying the grammar
+extensions, you may be more interested in the location of the error in
+the .ml4-preprocessed file, so that you can see what your new grammar
+extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1
+option. This will make compilation of a .ml4 file a two-stage process:
+
+1) create the .ml4-preprocessed file with camlp4o
+2) compile it with straight ocamlc/opt without preprocessor
+
+and will instruct make not to delete .ml4-preprocessed files
+automatically just because they are intermediary files, so that you
+can inspect them.
+
+If you add a _new_ grammar extension to Coq:
+
+ - if it can be built at stage1, that is the .ml4 file does not use a
+   Coq grammar extension itself, then add it, and all .cmo files it
+   needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the
+   handling of grammar.cma and q_constr.cmo for an example.
+
+ - if it cannot be built at stage1, that is the .ml4 file itself needs
+   to be preprocessed with a Coq camlp4 grammar extension, then,
+   congratulations, you need to add a new stage between stage1 and
+   stage2.
+
+New files
+---------
+
+For a new file, in most cases, you just have to add it to the proper
+file list(s) in Makefile.common, such as ARITHVO or TACTICS.
+
+The list of all ml4 files is not handled manually anymore.
+
+Exceptions are:
+
+ - The file is necessary at stage1, that it is necessary to build the
+   Coq camlp4 grammar extensions. In this case, make sure it ends up
+   in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of
+   grammar.cma and/or q_constr.cmo for an example.
+
+ - if the file needs to be compiled with -rectypes, add it to
+   RECTYPESML in Makefile.common. If it is a .ml4 file, implement
+   RECTYPESML4 or '(*i ocamlflags i*)'; see TODO.
+
+ - the file needs a specific Makefile entry; add it to Makefile.build
+
+ - the files produced from the added file do not match an existing
+   pattern or entry in "Makefile". (All the common cases of
+   .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively)
+   .cm[iox], .vo, .glob, .o, ... files with the same basename are
+   already covered.) In this case, see section "New targets".
+
+New targets
+-----------
+
+If you want to add:
+
+ - a new PHONY target to the build system, that is a target that is
+   not the name of the file it creates,
+
+ - a normal target is not already mapped to a stage by "Makefile"
+
+ then:
+
+ - add the necessary rule to Makefile.build, if any
+ - add the target to STAGEn_TARGETS, with n being the smallest stage
+   it can be built at, that is:
+   * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension
+   * 2 for OCaml code that uses (directly or indirectly) a Coq
+       camlp4 grammar extension. Indirectly means a dependency of it
+       does.
+   * 3 for Coq (.v) code.
+
+   *or*
+
+   add a pattern matching the target to the pattern lists for the
+   smallest stage it can be built at in "Makefile".
+
+TODO
+----
+
+delegate pa_extend.cmo to camlp4use statements and remove it from
+standard camlp4 options.
+
+maybe manage compilation flags (such as -rectypes or the CoqIDE ones)
+from a
+ (*i ocamlflags: "-rectypes" i*)
+statement in the .ml(4) files themselves, like camlp4use. The CoqIDE
+files could have
+ (*i ocamlflags: "${COQIDEFLAGS}" i*)
+and COQIDEFLAGS is still defined (and exported by) the Makefile.build.
+
+Clean up doc/Makefile
+
+config/Makefile looks like it contains a lot of unused variables,
+clean that up (are any maybe used by nightly scripts on
+pauillac?). Also, the COQTOP variable from config/Makefile (and used
+in contribs) has a very poorly chosen name, because "coqtop" is the
+name of a Coq executable! For example, in the Coq makefile it is
+immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or
+COQTREE or COQDIR or ...
+
+Promote the granular .glob handling to official way of doing things
+for Coq developments, that is implement it in coq_makefile and the
+contribs. Here are a few hints:
+
+>> Les fichiers de constantes produits par -dump-glob sont maintenant
+>> produits par fichier et sont ensuite concaténés dans
+>> glob.dump. Ilsont produits par défaut (avec les bonnes
+>> dépendances).
+
+> C'est une chose que l'on voulait faire aussi.
+
+(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.)
+
+> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de
+> la même façon
+
+Dans cette optique, il serait alors plus propre de changer coqdep pour
+qu'il produise directement l'output que nous mettons maintenant dans
+les .v.d (qui est celui de coqdoc post-processé avec sed).
+
+Si cette manière de gérer les glob devient le standard béni
+officiellement par "the Coq development team", ne voudrions nous pas
+changer coqc pour qu'il produise FOO.glob lors de la compilation de
+FOO.v par défaut (sans argument "-dump-glob")?
+
+> et que la production de a.html par coqdoc n'ait une dépendance qu'en
+> les a.v et a.glob correspondant ?
+
+Je crois que coqdoc exige un glob-dump unique, il convient donc de
+concaténer les .glob correspondants. Soit un glob-dump global par
+projet (par Makefile), soit un glob-dump global par .v(o), qui
+contient son .glob et ceux de tous les .v(o) atteignables par le
+graphe des dépendances. CoRN contient déjà un outil de calcul de
+partie atteignable du graphe des dépendances (il y est pour un autre
+usage, pour calculer les .v à mettre dans les différents tarballs sur
+http://corn.cs.ru.nl/download.html; les parties partielles sont
+définies par liste de fichiers .v + toutes leurs dépendances
+(in)directes), il serait alors adéquat de le mettre dans les tools de
+Coq.
+
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 90e29496..b7545e09 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,37 @@
 =========================================
+= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.1 and V8.2
+================================================================
+
+** Datatypes
+
+List of occurrences moved from "int list" to "Termops.occurrences" (an
+alias to "bool * int list").
+
+** Functions
+
+Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
+Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
+Eauto.simplest_apply -> Hiddentac.h_simplest_apply
+Evarutil.define_evar_as_arrow -> define_evar_as_product
+
+** Universe names (univ.mli)
+
+ base_univ -> type0_univ  (* alias of Set is the Type hierarchy *)
+ prop_univ -> type1_univ  (* the type of Set in the Type hierarchy *)
+ neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
+ is_base_univ -> is_type1_univ
+ is_empty_univ -> is_lower_univ
+
+** Sort names (term.mli)
+
+  mk_Set -> set_sort
+  mk_Prop -> prop_sort
+  type_0 -> type1_sort
+
+=========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
 =========================================
 
diff --git a/dev/doc/header b/dev/doc/header
deleted file mode 100644
index 57945e47..00000000
--- a/dev/doc/header
+++ /dev/null
@@ -1,7 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion
new file mode 100644
index 00000000..6274275c
--- /dev/null
+++ b/dev/doc/notes-on-conversion
@@ -0,0 +1,73 @@
+(**********************************************************************)
+(* A few examples showing the current limits of the conversion algorithm *)
+(**********************************************************************)
+
+(*** We define (pseudo-)divergence from Ackermann function ***)
+
+Definition ack (n : nat) :=
+  (fix F (n0 : nat) : nat -> nat :=
+     match n0 with
+     | O => S
+     | S n1 =>
+         fun m : nat =>
+         (fix F0 (n2 : nat) : nat :=
+            match n2 with
+            | O => F n1 1
+            | S n3 => F n1 (F0 n3)
+            end) m
+     end) n.
+
+Notation OMEGA := (ack 4 4).
+
+Definition f (x:nat) := x.
+
+(* Evaluation in tactics can somehow be controled *)
+Lemma l1 : OMEGA = OMEGA.
+reflexivity.  (* succeed: identity *)
+Qed.          (* succeed: identity *)
+
+Lemma l2 : OMEGA = f OMEGA.
+reflexivity.  (* fail: conversion wants to convert OMEGA with f OMEGA *)
+Abort.        (* but it reduces the right side first! *)
+
+Lemma l3 : f OMEGA = OMEGA.
+reflexivity.  (* succeed: reduce left side first *)
+Qed.          (* succeed: expected concl (the one with f) is on the left *)
+
+Lemma l4 : OMEGA = OMEGA.
+assert (f OMEGA = OMEGA) by reflexivity. (* succeed *)
+unfold f in H.   (* succeed: no type-checking *)
+exact H.         (* succeed: identity *)
+Qed.             (* fail: "f" is on the left *)
+
+(* This example would fail whatever the preferred side is *)
+Lemma l5 : OMEGA = f OMEGA.
+unfold f.
+assert (f OMEGA = OMEGA) by reflexivity.
+unfold f in H.
+exact H.
+Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *)
+
+(**********************************************************************)
+(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *)
+(* (proof of span_ind_uninject_prop *)
+
+In the proof, a problem of the form   (Equal S t1 t2)
+is "simpl"ified, then "red"uced to    (Equal S' t1 t1)
+where the new t1's are surrounded by invisible coercions.
+A reflexivity steps conclude the proof.
+
+The trick is that Equal projects the equality in the setoid S, and
+that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)).
+
+At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1)
+and the algorithm is to first compare S and S', and t1 and t2.
+Unfortunately it does not work, and since t1 and t2 involve concrete
+instances of algebraic structures, it takes a lot of time to realize that
+it is not convertible.
+
+The only hope to improve this problem is to observe that S' hides
+(behind two indirections) a Setoid constructor. This could be the
+argument to solve the problem.
+
+
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index f4cb3bff..8e481544 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,13 +1,79 @@
-Performance analysis for V8-0 branch
-------------------------------------
+Performance analysis (trunk repository)
+---------------------------------------
 
-Oct 29, 2006: polymorphism on definitions (+ 4%)
+May 21, 2008: New version of CoRN
+  (needs +84% more time to compile)
+
+Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu)
+  (+28% CoRN) 
+
+Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug
+  fixes, control of zeta in rewrite, auto (??))
+  (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg,
+  but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%)
+
+Mar 11, 2008:
+  (+19% PersistentUnionFind wrt Mar 3, +21% Angles, 
+   +270% Continuations between 7/3 and 18/4)
+
+Mar 7, 2008:
+  (-10% PersistentUnionFind wrt Mar 3)
+
+Feb 20, 2008: temporary 1-day slow down
+  (+64% LinAlg)
+
+Feb 14, 2008:
+  (-10% PersistentUnionFind, -19% Groups)
+
+Feb 7, 8, 2008: temporary 2-days long slow down
+  (+20 LinAlg, +50% BDDs)
+
+Feb 2, 2008: many updates of the module system
+  (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, 
+   -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices)
+
+Jan 1, 2008: merge of TypeClasses branch
+  (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel)
+
+Nov 16, 17, 2007:
+  (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days)
+
+Nov 8, 2007:
+  (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL,
+   +220% SquareMatrices)
+
+Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables)
+
+Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the
+  tactic interpreter (from revision 10222 to 10267)
+  (+22% CoRN, +10% geometry, ...)
+
+Sep 16, 2007:
+  (+16% PersistentUnionFind on 3 days, LinAlg stable,
+
+Sep 4, 2007:
+  (+26% PersistentUnionFind, LinAlg stable,
+
+Jun 6, 2007: optimization of the need for type unification in with-bindings
+  (-3.5% Stalmark, -6% Kildall)
+
+May 20, 21, 22, 2007: improved inference of with-bindings (including activation
+  of unification on types)
+  (+4% PICALC, +5% Stalmark, +7% Kildall)
+
+May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...)
+
+Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's
+  computer (-25% CoRN, -25% Fairisle, ...)
+
+Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions
+  (+4% in general during these two days)
 
 Oct 17, 2006: improvement in new field [r9248]
   (QArith -3%, geometry: -2%)
 
 Oct 5, 2006: fixing wrong unification of Meta below binders
-  (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, 
+  (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%,
    DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%)
 
 Sep 26, 2006: new field [r9178-9181]
@@ -17,11 +83,17 @@ Sep 26, 2006: new field [r9178-9181]
   Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s)
   May 30, 2006: Nancy/CoLoR added (~ 319s)
 
+May 23, 2006: new, lighter version of polymorphic inductive types
+  (CoRN: -27%, back to Mar-24 time)
+
 May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -)
 
 May 5, 2006: improvement in closure (array instead of lists)
   (e.g. CatsInZFC: -10%, CoRN: -3%, 
 
+May 23, 2006: polymorphic inductive types (precise, heavy algorithm)
+  (CoRN: +37%)
+
   Dec 29, 2005: new test and use of -vm in Stalmarck
 
   Dec 27, 2005: contrib Karatsuba added (~ 30s)