Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder.

8 files changed, 2272 insertions, 0 deletions

diff --git a/dev/doc/archive/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY
new file mode 100644
index 0000000000..a81afca32d
--- /dev/null
+++ b/dev/doc/archive/COMPATIBILITY
@@ -0,0 +1,201 @@
+Note: this file isn't used anymore. Incompatibilities are documented
+as part of CHANGES.
+
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+  error rather than a warning when the superfluous name is already in
+  use. The easy fix is to remove the superfluous name.
+
+Potential sources of incompatibilities between Coq V8.5 and V8.6
+----------------------------------------------------------------
+
+Symptom: An obligation generated by Program or an abstracted subproof
+has different arguments.
+Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+and the subproof does not use the argument.
+Remedy:
+- Adapt the script.
+- Write an explicit lemma to prove the obligation/subproof and use it
+  instead (compatible with 8.4).
+- Unset the option for the program/proof the obligation/subproof originates
+  from.
+
+Symptom: In a goal, order of hypotheses, or absence of an equality of
+the form "x = t" or "t = x", or no unfolding of a local definition.
+Cause: This might be connected to a number of fixes in the tactic
+"subst". The former behavior can be reactivated by issuing "Unset
+Regular Subst Tactic".
+  
+Potential sources of incompatibilities between Coq V8.4 and V8.5
+----------------------------------------------------------------
+
+* List of typical changes to be done to adapt files from Coq 8.4 *
+* to Coq 8.5 when not using compatibility option "-compat 8.4".  *
+
+Symptom: "The reference omega was not found in the current environment".
+Cause: "Require Omega" does not import the tactic "omega" any more
+Possible solutions:
+- use "Require Import OmegaTactic" (not compatible with 8.4)
+- use "Require Import Omega" (compatible with 8.4)
+- add definition "Ltac omega := Coq.omega.Omega.omega."
+  
+Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
+Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
+Possible solutions:
+- use "dintuition" instead; it is stronger than "intuition" and works
+  uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
+  (not compatible with 8.4)
+- do the script differently
+
+Symptom: The constructor foo (in type bar) expects n arguments.
+Cause: parameters must now be given in patterns
+Possible solutions:
+- use option "Set Asymmetric Patterns" (compatible with 8.4)
+- add "_" for the parameters (not compatible with 8.4)
+- turn the parameters into implicit arguments (compatible with 8.4)
+
+Symptom: "NPeano.Nat.foo" not existing anymore
+Possible solutions:
+- use "Nat.foo" instead
+
+Symptom: typing problems with proj1_sig or similar
+Cause: coercion from sig to sigT and similar coercions have been
+  removed so as to make the initial state easier to understand for
+  beginners
+Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
+
+* Other detailed changes *
+
+(see also file CHANGES)
+
+- options for *coq* compilation (see below for ocaml).
+
+** [-I foo] is now deprecated and will not add directory foo to the
+   coq load path (only for ocaml, see below). Just replace [-I foo] by
+   [-Q foo ""] in your project file and re-generate makefile. Or
+   perform the same operation directly in your makefile if you edit it
+   by hand.
+
+** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
+   load path.
+
+** Option [-I foo -as bar] is unchanged but discouraged unless you
+   compile ocaml code. Use -Q foo bar instead.
+
+  for more details: file CHANGES or section "Customization at launch
+  time" of the reference manual.
+
+- Command line options for ocaml  Compilation of ocaml code (plugins) 
+
+** [-I foo] is *not* deprecated to add foo to the ocaml load path.
+
+** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
+   the coq load path with logical name bar (shortcut for -I foo -Q foo
+   bar).
+
+  for more details: file CHANGES or section "Customization at launch
+  time" of the reference manual.
+
+- Universe Polymorphism.
+
+- Refinement, unification and tactics are now aware of universes,
+  resulting in more localized errors. Universe inconsistencies 
+  should no more get raised at Qed time but during the proof.
+  Unification *always* produces well-typed substitutions, hence
+  some rare cases of unifications that succeeded while producing
+  ill-typed terms before will now fail.
+  
+- The [change p with c] tactic semantics changed, now typechecking 
+  [c] at each matching occurrence [t] of the pattern [p], and 
+  converting [t] with [c].
+  
+- Template polymorphic inductive types: the partial application 
+  of a template polymorphic type (e.g. list) is not polymorphic.
+  An explicit parameter application (e.g [fun A => list A]) or
+  [apply (list _)] will result in a polymorphic instance.
+
+- The type inference algorithm now takes opacity of constants into
+  account. This may have effects on tactics using type inference
+  (e.g. induction). Extra "Transparent" might have to be added to
+  revert opacity of constants.
+
+Type classes.
+
+- When writing an Instance foo : Class A := {| proj := t |} (note the
+  vertical bars), support for typechecking the projections using the
+  type information and switching to proof mode is no longer available.
+  Use { } (without the vertical bars) instead.
+
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+  the global environment and inlined in the proof term when a proof
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
+  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
+
+Potential sources of incompatibilities between Coq V8.3 and V8.4
+----------------------------------------------------------------
+
+(see also file CHANGES)
+
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+  Several definitions have new names or are defined in modules of
+  different names, but a special care has been taken to have this
+  renaming transparent for the user thanks to compatibility notations.
+
+  However some definitions have changed, what might require some
+  adaptations. The most noticeable examples are:
+  - The "?=" notation which now bind to Pos.compare rather than former
+    Pcompare (now Pos.compare_cont).
+  - Changes in names may induce different automatically generated
+    names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+  - Z.add has a new definition, hence, applying "simpl" on subterms of
+    its body might give different results than before.
+  - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+    power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+  - The definition of functions over "vectors" (list of fixed length)
+    have changed.
+  - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+  - Less unfolding of fixpoints when applying destruct or inversion on
+    a fixpoint hiding an inductive type (add an extra call to simpl to
+    preserve compatibility).
+  - Less unexpected local definitions when applying "destruct"
+    (incompatibilities solvable by adapting name hypotheses).
+  - Tactic "apply" might succeed more often, e.g. by now solving
+    pattern-matching of the form ?f x y = g(x,y) (compatibility
+    ensured by using "Unset Tactic Pattern Unification"), but also
+    because it supports (full) betaiota (using "simple apply" might
+    then help).
+  - Tactic autorewrite does no longer instantiate pre-existing
+    existential variables.
+  - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+  - The command "Load" is now atomic for backtracking (use "Unset
+    Atomic Load" for compatibility).
+
+
+Incompatibilities beyond 8.4...
+
+- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
+  now "A -> (B <-> C)"
+
+- Tactics: tauto and intuition no longer accidentally destruct binary
+  connectives or records other than and, or, prod, sum, iff. In most
+  of cases, dtauto or dintuition, though stronger than 8.3 tauto and
+  8.3 intuition will provide compatibility.
+
+- "Solve Obligations using" is now "Solve Obligations with".
diff --git a/dev/doc/archive/extensions.txt b/dev/doc/archive/extensions.txt
new file mode 100644
index 0000000000..36d63029f1
--- /dev/null
+++ b/dev/doc/archive/extensions.txt
@@ -0,0 +1,18 @@
+Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ?
+======================================================================
+
+Exemple de l'ajout de l'entrée "clause":
+
+- ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les
+  wit_, rawwit_, et globwit_ correspondants
+
+- ajouter partout où Genarg.argument_type est filtré le cas traitant de
+  ce nouveau ClauseArgType
+
+- utiliser le rawwit_clause pour définir une entrée clause du bon
+  type et du bon nom dans le module Tactic de pcoq.ml4
+
+- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il
+  faut rejouter clause dans le GLOBAL du GEXTEND
+
+- seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex
new file mode 100644
index 0000000000..0b0811d81b
--- /dev/null
+++ b/dev/doc/archive/naming-conventions.tex
@@ -0,0 +1,606 @@
+\documentclass[a4paper]{article}
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{amsfonts}
+
+\parindent=0pt
+\parskip=10pt
+
+%%%%%%%%%%%%%
+% Macros
+\newcommand\itemrule[3]{
+\subsubsection{#1}
+\begin{quote}
+\begin{tt}
+#3
+\end{tt}
+\end{quote}
+\begin{quote}
+Name: \texttt{#2}
+\end{quote}}
+
+\newcommand\formula[1]{\begin{tt}#1\end{tt}}
+\newcommand\tactic[1]{\begin{tt}#1\end{tt}}
+\newcommand\command[1]{\begin{tt}#1\end{tt}}
+\newcommand\term[1]{\begin{tt}#1\end{tt}}
+\newcommand\library[1]{\texttt{#1}}
+\newcommand\name[1]{\texttt{#1}}
+
+\newcommand\zero{\texttt{zero}}
+\newcommand\op{\texttt{op}}
+\newcommand\opPrime{\texttt{op'}}
+\newcommand\opSecond{\texttt{op''}}
+\newcommand\phimapping{\texttt{phi}}
+\newcommand\D{\texttt{D}}
+\newcommand\elt{\texttt{elt}}
+\newcommand\rel{\texttt{rel}}
+\newcommand\relp{\texttt{rel'}}
+
+%%%%%%%%%%%%%
+
+\begin{document}
+
+\begin{center}
+\begin{huge}
+Proposed naming conventions for the Coq standard library
+\end{huge}
+\end{center}
+\bigskip
+
+The following document describes a proposition of canonical naming
+schemes for the Coq standard library. Obviously and unfortunately, the
+current state of the library is not as homogeneous as it would be if
+it would systematically follow such a scheme. To tend in this
+direction, we however recommend to follow the following suggestions.
+
+\tableofcontents
+
+\section{General conventions}
+
+\subsection{Variable names}
+
+\begin{itemize}
+
+\item Variables are preferably quantified at the head of the
+  statement, even if some premisses do not depend of one of them. For
+  instance, one would state
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, x <= y -> x+z <= y+z}
+\end{tt}
+\end{quote}
+and not
+\begin{quote}
+\begin{tt}
+  {forall x y:D, x <= y -> forall z:D, x+z <= y+z}
+\end{tt}
+\end{quote}
+
+\item Variables are preferably quantified (and named) in the order of
+  ``importance'', then of appearance, from left to right, even if
+  for the purpose of some tactics it would have been more convenient
+  to have, say, the variables not occurring in the conclusion
+  first. For instance, one would state
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, x+z <= y+z -> x <= y}
+\end{tt}
+\end{quote}
+and not
+\begin{quote}
+\begin{tt}
+  {forall z x y:D, x+z <= y+z -> x <= y}
+\end{tt}
+\end{quote}
+nor
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, y+x <= z+x -> y <= z}
+\end{tt}
+\end{quote}
+
+\item Choice of effective names is domain-dependent. For instance, on
+  natural numbers, the convention is to use the variables $n$, $m$,
+  $p$, $q$, $r$, $s$ in this order.
+
+  On generic domains, the convention is to use the letters $x$, $y$,
+  $z$, $t$. When more than three variables are needed, indexing variables
+
+  It is conventional to use specific names for variables having a
+  special meaning. For instance, $eps$ or $\epsilon$ can be used to
+  denote a number intended to be as small as possible. Also, $q$ and
+  $r$ can be used to denote a quotient and a rest. This is good
+  practice.
+
+\end{itemize}
+
+\subsection{Disjunctive statements}
+
+A disjunctive statement with a computational content will be suffixed
+by \name{\_inf}. For instance, if
+
+\begin{quote}
+\begin{tt}
+{forall x y, op x y = zero -> x = zero \/ y = zero}
+\end{tt}
+\end{quote}
+has name \texttt{D\_integral}, then
+\begin{quote}
+\begin{tt}
+{forall x y, op x y = zero -> \{x = zero\} + \{y = zero\}}
+\end{tt}
+\end{quote}
+will have name \texttt{D\_integral\_inf}.
+
+As an exception, decidability statements, such as
+\begin{quote}
+\begin{tt}
+{forall x y, \{x = y\} + \{x <> y\}}
+\end{tt}
+\end{quote}
+will have a named ended in \texttt{\_dec}. Idem for cotransitivity
+lemmas which are inherently computational that are ended in
+\texttt{\_cotrans}.
+
+\subsection{Inductive types constructor names}
+
+As a general rule, constructor names start with the name of the
+inductive type being defined as in \texttt{Inductive Z := Z0 : Z |
+  Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard
+types like \texttt{bool}, \texttt{nat}, \texttt{list}...
+
+For inductive predicates, constructor names also start with the name
+of the notion being defined with one or more suffixes separated with
+\texttt{\_} for discriminating the different cases as e.g. in
+
+\begin{verbatim}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S n : odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S n : even n -> odd (S n).
+\end{verbatim}
+
+As a general rule, inductive predicate names should be lowercase (to
+the exception of notions referring to a proper name, e.g. \texttt{Bezout})
+and multiple words must be separated by ``{\_}''.
+
+As an exception, when extending libraries whose general rule is that
+predicates names start with a capital letter, the convention of this
+library should be kept and the separation between multiple words is
+done by making the initial of each work a capital letter (if one of
+these words is a proper name, then a ``{\_}'' is added to emphasize
+that the capital letter is proper and not an application of the rule
+for marking the change of word).
+
+Inductive predicates that characterize the specification of a function
+should be named after the function it specifies followed by
+\texttt{\_spec} as in:
+
+\begin{verbatim}
+Inductive nth_spec : list A -> nat -> A -> Prop :=
+  | nth_spec_O a l : nth_spec (a :: l) 0 a
+  | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a.
+\end{verbatim}
+
+\section{Equational properties of operations}
+
+\subsection{General conventions}
+
+If the conclusion is in the other way than listed below, add suffix
+\name{\_reverse} to the lemma name.
+
+\subsection{Specific conventions}
+
+\itemrule{Associativity of binary operator {\op} on domain {\D}}{Dop\_assoc}
+{forall x y z:D, op x (op y z) = op (op x y) z}
+
+  Remark: Symmetric form: \name{Dop\_assoc\_reverse}:
+  \formula{forall x y z:D, op (op x y) z = op x (op y z)}
+
+\itemrule{Commutativity of binary operator {\op} on domain {\D}}{Dop\_comm}
+{forall x y:D, op x y = op y x}
+
+  Remark: Avoid \formula{forall x y:D, op y x = op x y}, or at worst, call it
+  \name{Dop\_comm\_reverse}
+
+\itemrule{Left neutrality of element elt for binary operator {\op}}{Dop\_elt\_l}
+{forall x:D, op elt x = x}
+
+  Remark: In English, ``{\elt} is an identity for {\op}'' seems to be
+  a more common terminology.
+
+\itemrule{Right neutrality of element elt for binary operator {\op}}{Dop\_elt\_r}
+{forall x:D, op x elt = x}
+
+  Remark: By convention, if the identities are reminiscent to zero or one, they
+  are written 1 and 0 in the name of the property.
+
+\itemrule{Left absorption of element elt for binary operator {\op}}{Dop\_elt\_l}
+{forall x:D, op elt x = elt}
+
+  Remarks:
+  \begin{itemize}
+  \item In French school, this property is named "elt est absorbant pour op"
+  \item English, the property seems generally named "elt is a zero of op"
+  \item In the context of lattices, this a boundedness property, it may
+     be called "elt is a bound on D", or referring to a (possibly
+     arbitrarily oriented) order "elt is a least element of D" or "elt
+     is a greatest element of D"
+  \end{itemize}
+
+\itemrule{Right absorption of element {\elt} for binary operator {\op}}{Dop\_elt\_l  [BAD ??]}
+{forall x:D, op x elt = elt}
+
+\itemrule{Left distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_l}
+{forall x y z:D, op (op' x y) z = op' (op x z) (op y z)}
+
+  Remark: Some authors say ``distribution''.
+
+\itemrule{Right distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_r}
+{forall x y z:D, op z (op' x y) = op' (op z x) (op z y)}
+
+  Remark: Note the order of arguments.
+
+\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
+{forall x y:D, op (op' x y) = op' (op x) (op y)}
+
+\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
+{forall x y:D, op (op' x y) = op' (op x) (op y)}
+
+  Remark: For a non commutative operation with inversion of arguments, as in
+  \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)},
+  we may probably still call the property distributivity since there
+  is no ambiguity.
+
+  Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}.
+
+  Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}.
+
+\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l}
+{forall x y:D, op (op' x y) = op' (op x) y}
+
+  Question: Call it left commutativity ?? left swap ?
+
+\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r}
+{forall x y:D, op (op' x y) = op' x (op y)}
+
+\itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
+{forall x:D, op x x = x}
+
+\itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent}
+{forall x:D, op (op x) = op x}
+
+  Remark: This is actually idempotency of {\op} wrt to composition and
+  identity.
+
+\itemrule{Idempotency of element elt for binary operator {\op} on domain {\D}}{Dop\_elt\_idempotent}
+{op elt elt = elt}
+
+  Remark: Generally useless in CIC for concrete, computable operators
+
+  Remark: The general definition is ``exists n, iter n op x = x''.
+
+\itemrule{Nilpotency of element elt wrt a ring D with additive neutral
+element {\zero} and multiplicative binary operator
+{\op}}{Delt\_nilpotent}
+{op elt elt = zero}
+
+  Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''.
+
+\itemrule{Zero-product property in a ring D with additive neutral
+element {\zero} and multiplicative binary operator
+{\op}}{D\_integral}
+{forall x y, op x y = zero -> x = zero \/ y = zero}
+
+  Remark: We leave the ring structure of D implicit; the Coq library
+  uses either \texttt{\_is\_O} (for \texttt{nat}), \texttt{\_integral}
+    (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for
+    \texttt{NZ}).
+
+  Remark: The French school says ``integrité''.
+
+\itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element
+zero in D}{Dop\_nilpotent} {forall x, op x x = zero}
+
+  Remark: Did not find this definition on the web, but it used in
+  the Coq library (to characterize \name{xor}).
+
+\itemrule{Involutivity of unary op on D}{Dop\_involutive}
+{forall x:D, op (op x) = x}
+
+\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the left}{Dop\_op'\_absorption\_l\_l}
+{forall x y:D, op x (op' x y) = x}
+
+\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the right}{Dop\_op'\_absorption\_l\_r}
+{forall x y:D, op x (op' y x) = x}
+
+  Remark: Similarly for \name{Dop\_op'\_absorption\_r\_l} and \name{Dop\_op'\_absorption\_r\_r}.
+
+\itemrule{De Morgan law's for binary operators {\opPrime} and {\opSecond} wrt
+to unary op on domain {\D}}{Dop'\_op''\_de\_morgan,
+Dop''\_op'\_de\_morgan ?? \mbox{leaving the complementing operation
+implicit})}
+{forall x y:D, op (op' x y) = op'' (op x) (op y)\\
+forall x y:D, op (op'' x y) = op' (op x) (op y)}
+
+\itemrule{Left complementation of binary operator {\op} by means of unary {\opPrime} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_op'\_opp\_l}
+{forall x:D, op (op' x) x = elt}
+
+Remark: If the name of the opposite function is reminiscent of the
+notion of complement (e.g. if it is called \texttt{opp}), one can
+simply say {Dop\_opp\_l}.
+
+\itemrule{Right complementation of binary operator {\op} by means of unary {\op'} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_opp\_r}
+{forall x:D, op x (op' x) = elt}
+
+Example: \formula{Radd\_opp\_l: forall r : R, - r + r = 0}
+
+\itemrule{Associativity of binary operators {\op} and {\op'}}{Dop\_op'\_assoc}
+{forall x y z, op x (op' y z) = op (op' x y) z}
+
+Example: \formula{forall x y z, x + (y - z) = (x + y) - z}
+
+\itemrule{Right extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_r}
+{forall x y z, op x (op' y z) = op' (op x y) z}
+
+Remark: This requires {\op} and {\opPrime} to have their right and left
+argument respectively and their return types identical.
+
+Example: \formula{forall x y z, x + (y - z) = (x + y) - z}
+
+Remark: Other less natural combinations are possible, such
+as \formula{forall x y z, op x (op' y z) = op' y (op x z)}.
+
+\itemrule{Left extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_l}
+{forall x y z, op (op' x y) z = op' x (op y z)}
+
+Remark: Operations are not necessarily internal composition laws.  It
+is only required that {\op} and {\opPrime} have their right and left
+argument respectively and their return type identical.
+
+Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}.
+
+Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}.
+
+%======================================================================
+%\section{Properties of elements}
+
+%Remark: Not used in current library
+
+
+
+%======================================================================
+\section{Preservation and compatibility properties of operations}
+
+\subsection{With respect to equality}
+
+\itemrule{Injectivity of unary operator {\op}}{Dop\_inj}
+{forall x y:D, op x = op y -> x = y}
+
+\itemrule{Left regularity of binary operator {\op}}{Dop\_reg\_l, Dop\_inj\_l, or Dop\_cancel\_l}
+{forall x y z:D, op z x = op z y -> x = y}
+
+  Remark: Note the order of arguments.
+
+  Remark: The Coq usage is to called it regularity but the English
+  standard seems to be cancellation. The recommended form is not
+  decided yet.
+
+  Remark: Shall a property like $n^p \leq n^q \rightarrow p \leq q$
+  (for $n\geq 1$) be called cancellation or should it be reserved for
+  operators that have an inverse?
+
+\itemrule{Right regularity of binary operator {\op}}{Dop\_reg\_r, Dop\_inj\_r, Dop\_cancel\_r}
+{forall x y z:D, op x z = op y z -> x = y}
+
+\subsection{With respect to a relation {\rel}}
+
+\itemrule{Compatibility of unary operator {\op}}{Dop\_rel\_compat}
+{forall x y:D, rel x y -> rel (op x) (op y)}
+
+\itemrule{Left compatibility of binary operator {\op}}{Dop\_rel\_compat\_l}
+{forall x y z:D, rel x y -> rel (op z x) (op z y)}
+
+\itemrule{Right compatibility of binary operator {\op}}{Dop\_rel\_compat\_r}
+{forall x y z:D, rel x y -> rel (op x z) (op y z)}
+
+  Remark: For equality, use names of the form \name{Dop\_eq\_compat\_l} or
+  \name{Dop\_eq\_compat\_r}
+(\formula{forall x y z:D, y = x -> op y z = op x z} and
+\formula{forall x y z:D, y = x -> op y z = op x z})
+
+  Remark: Should we admit (or even prefer) the name
+  \name{Dop\_rel\_monotone}, \name{Dop\_rel\_monotone\_l},
+  \name{Dop\_rel\_monotone\_r} when {\rel} is an order ?
+
+\itemrule{Left regularity of binary operator {\op}}{Dop\_rel\_reg\_l}
+{forall x y z:D, rel (op z x) (op z y) -> rel x y}
+
+\itemrule{Right regularity of binary operator {\op}}{Dop\_rel\_reg\_r}
+{forall x y z:D, rel (op x z) (op y z) -> rel x y}
+
+  Question: Would it be better to have \name{z} as first argument, since it
+  is missing in the conclusion ?? (or admit we shall use the options
+  ``\texttt{with p}''?)
+
+\itemrule{Left distributivity of binary operator {\op} over {\opPrime} along relation {\rel} on domain {\D}}{Dop\_op'\_rel\_distr\_l}
+{forall x y z:D, rel (op (op' x y) z) (op' (op x z) (op y z))}
+
+  Example: standard property of (not necessarily distributive) lattices
+
+  Remark: In a (non distributive) lattice, by swapping join and meet,
+  one would like also,
+\formula{forall x y z:D, rel (op' (op x z) (op y z)) (op (op' x y) z)}.
+  How to name it with a symmetric name (use
+ \name{Dop\_op'\_rel\_distr\_mon\_l} and
+ \name{Dop\_op'\_rel\_distr\_anti\_l})?
+
+\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm}
+{forall x y z:D, rel (op x y) (op y x)}
+
+  Example:
+\formula{forall l l':list A, Permutation (l++l') (l'++l)}
+
+\itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible}
+{forall x y z:D, z = op x y -> z = x $\backslash/$ z = y}
+
+  Question: What about the constructive version ? Call it \name{Dop\_irreducible\_inf} ?
+\formula{forall x y z:D, z = op x y -> \{z = x\} + \{z = y\}}
+
+\itemrule{Primality of binary operator {\op} along relation {\rel} on domain {\D}}{Dop\_rel\_prime}
+{forall x y z:D, rel z (op x y) -> rel z x $\backslash/$ rel  z y}
+
+
+%======================================================================
+\section{Morphisms}
+
+\itemrule{Morphism between structures {\D} and {\D'}}{\name{D'\_of\_D}}{D -> D'}
+
+Remark: If the domains are one-letter long, one can used \texttt{IDD'} as for
+\name{INR} or \name{INZ}.
+
+\itemrule{Morphism {\phimapping} mapping unary operators {\op} to {\op'}}{phi\_op\_op', phi\_op\_op'\_morphism}
+{forall x:D, phi (op x) = op' (phi x)}
+
+Remark: If the operators have the same name in both domains, one use
+\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}.
+
+Example: \formula{Z\_of\_nat\_mult: forall n m : nat, Z\_of\_nat (n * m) = (Z\_of\_nat n * Z\_of\_nat m)\%Z}.
+
+Remark: If the operators have different names on distinct domains, one
+can use \texttt{op\_op'}.
+
+\itemrule{Morphism {\phimapping} mapping binary operators {\op} to
+{\op'}}{phi\_op\_op', phi\_op\_op'\_morphism}  {forall
+x y:D, phi (op x y) = op' (phi x) (phi y)}
+
+Remark: If the operators have the same name in both domains, one use
+\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}.
+
+Remark: If the operators have different names on distinct domains, one
+can use \texttt{op\_op'}.
+
+\itemrule{Morphism {\phimapping} mapping binary operator {\op} to
+binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism}
+{forall x y:D, phi (op x y) <-> rel (phi x) (phi y)}
+
+Remark: If the operator and the relation have similar name, one uses
+\texttt{phi\_op}.
+
+Question: How to name each direction? (add \_elim for -> and \_intro
+for <- ?? -- as done in Bool.v ??)
+
+Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}.
+
+%======================================================================
+\section{Preservation and compatibility properties of operations wrt order}
+
+\itemrule{Compatibility of binary operator {\op} wrt (strict order) {\rel} and (large order) {\rel'}}{Dop\_rel\_rel'\_compat}
+{forall x y z t:D, rel x y -> rel' z t -> rel (op x z) (op y t)}
+
+\itemrule{Compatibility of binary operator {\op} wrt (large order) {\relp} and (strict order) {\rel}}{Dop\_rel'\_rel\_compat}
+{forall x y z t:D, rel' x y -> rel z t -> rel (op x z) (op y t)}
+
+
+%======================================================================
+\section{Properties of relations}
+
+\itemrule{Reflexivity of relation {\rel} on domain {\D}}{Drel\_refl}
+{forall x:D, rel x x}
+
+\itemrule{Symmetry of relation {\rel} on domain {\D}}{Drel\_sym}
+{forall x y:D, rel x y -> rel y x}
+
+\itemrule{Transitivity of relation {\rel} on domain {\D}}{Drel\_trans}
+{forall x y z:D, rel x y -> rel y z -> rel x z}
+
+\itemrule{Antisymmetry of relation {\rel} on domain {\D}}{Drel\_antisym}
+{forall x y:D, rel x y -> rel y x -> x = y}
+
+\itemrule{Irreflexivity of relation {\rel} on domain {\D}}{Drel\_irrefl}
+{forall x:D, \~{} rel x x}
+
+\itemrule{Asymmetry of relation {\rel} on domain {\D}}{Drel\_asym}
+{forall x y:D, rel x y -> \~{} rel y x}
+
+\itemrule{Cotransitivity of relation {\rel} on domain {\D}}{Drel\_cotrans}
+{forall x y z:D, rel x y -> \{rel z y\} + \{rel x z\}}
+
+\itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy}
+{forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}}
+
+  Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or
+  \name{Drel\_connected}? Use
+  $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction,
+  for nicer elimination.
+
+\itemrule{Informative decidability of relation {\rel} on domain {\D}}{Drel\_dec (or Drel\_dect, Drel\_dec\_inf ?)}
+{forall x y:D, \{rel x y\} + \{\~{} rel x y\}}
+
+  Remark: If equality: \name{D\_eq\_dec} or \name{D\_dec} (not like
+  \name{eq\_nat\_dec})
+
+\itemrule{Non informative decidability of relation {\rel} on domain {\D}}{Drel\_dec\_prop (or Drel\_dec)}
+{forall x y:D, rel x y $\backslash/$ \~{} rel x y}
+
+\itemrule{Inclusion of relation {\rel} in relation {\rel}' on domain {\D}}{Drel\_rel'\_incl (or Drel\_incl\_rel')}
+{forall x y:D, rel x y -> rel' x y}
+
+  Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ??
+
+%======================================================================
+\section{Relations between properties}
+
+\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff}
+{forall x1 .. xn, P <-> Q}
+
+  Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to
+  recover what pertains to \texttt{P} and what pertains to \texttt{Q}
+  in their concatenation (as e.g. in
+  \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}).
+
+%======================================================================
+\section{Arithmetical conventions}
+
+\begin{minipage}{6in}
+\renewcommand{\thefootnote}{\thempfootnote}  % For footnotes...
+\begin{tabular}{lll}
+Zero on domain {\D} & D0 & (notation \verb=0=)\\
+One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\
+Successor on domain {\D} & Dsucc\\
+Predessor on domain {\D} & Dpred\\
+Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}}
+ & (infix notation \verb=+= [50,L])\\
+Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\
+Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\
+Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\
+Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\
+Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\
+Minimal element on domain {\D} & Dmin\\
+Maximal element on domain {\D} & Dmax\\
+Large less than order on {\D} & Dle & (infix notations \verb!<=! and \verb!>=! [70,N]))\\
+Strict less than order on {\D} & Dlt & (infix notations \verb=<= and \verb=>= [70,N]))\\
+\end{tabular}
+\bigskip
+\end{minipage}
+
+\bigskip
+
+The status of \verb!>=! and \verb!>! is undecided yet. It will eithet
+be accepted only as parsing notations or may also accepted as a {\em
+  definition} for the \verb!<=! and \verb!<! (like in \texttt{nat}) or
+even as a different definition (like it is the case in \texttt{Z}).
+
+\bigskip
+
+Exception: Peano Arithmetic which is used for pedagogical purpose:
+
+\begin{itemize}
+\item domain name is implicit
+\item \term{0} (digit $0$) is \term{O} (the 15th letter of the alphabet)
+\item \term{succ} is \verb!S! (but \term{succ} can be used in theorems)
+\end{itemize}
+
+\end{document}
diff --git a/dev/doc/archive/newsyntax.tex b/dev/doc/archive/newsyntax.tex
new file mode 100644
index 0000000000..71e964bcc9
--- /dev/null
+++ b/dev/doc/archive/newsyntax.tex
@@ -0,0 +1,725 @@
+
+%% -*-french-tex-*-
+
+\documentclass{article}
+
+\usepackage{verbatim}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[french]{babel}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{array}
+
+
+\author{B.~Barras}
+\title{Proposition de syntaxe pour Coq}
+
+%% Le _ est un caractère normal
+\catcode`\_=13
+\let\subscr=_
+\def_{\ifmmode\sb\else\subscr\fi}
+
+%% Macros pour les grammaires
+\def\NT#1{\langle\textit{#1}\rangle}
+\def\TERM#1{\textsf{#1}}
+\def\STAR#1{#1\!*}
+\def\PLUS#1{#1\!+}
+
+%% Tableaux de definition de non-terminaux
+\newenvironment{cadre}
+        {\begin{array}{|c|}\hline\\}
+        {\\\\\hline\end{array}}
+\newenvironment{rulebox}
+        {$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}r}}
+        {\end{array}\end{cadre}$$}
+\def\DEFNT#1{\NT{#1} & ::= &}
+\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&}
+\def\RNAME#1{(\textsc{#1})}
+\def\SEPDEF{\\\\}
+\def\nlsep{\\&|&}
+
+
+\begin{document}
+
+\maketitle
+
+\section{Grammaire des tactiques}
+\label{tacticsyntax}
+
+La réflexion de la rénovation de la syntaxe des tactiques n'est pas
+encore aussi poussée que pour les termes (section~\ref{constrsyntax}),
+mais cette section vise à énoncer les quelques principes que l'on
+souhaite suivre.
+
+\begin{itemize}
+\item Réutiliser les mots-clés de la syntaxe des termes (i.e. en
+  minuscules) pour les constructions similaires de tactiques (let_in,
+  match, and, etc.). Le connecteur logique \texttt{and} n'étant que
+  rarement utilisé autrement que sous la forme \texttt{$\wedge$} (sauf
+  dans le code ML), on pourrait dégager ce mot-clé.
+\item Les arguments passés aux tactiques sont principalement des
+  termes, on préconise l'utilisation d'un symbole spécial (par exemple
+  l'apostrophe) pour passer une tactique ou une expression
+  (AST). L'idée étant que l'on écrit plus souvent des tactiques
+  prenant des termes en argument que des tacticals.
+\end{itemize}
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{tactic}
+       \NT{tactic} ~\TERM{\&} ~\NT{tactic}            & \RNAME{then}
+\nlsep \TERM{[} ~\NT{tactic}~\TERM{|}~...
+      ~\TERM{|}~\NT{tactic}~\TERM{]}                  & \RNAME{par}
+\nlsep \NT{ident} ~\STAR{\NT{tactic-arg}}   ~~~       & \RNAME{apply}
+\nlsep \TERM{fun} ~....                               & \RNAME{function}
+\nlsep \NT{simple-tactic}
+\SEPDEF
+\DEFNT{tactic-arg}
+       \NT{constr}
+\nlsep \TERM{'} ~\NT{tactic}
+\SEPDEF
+\DEFNT{simple-tactic}
+       \TERM{Apply} ~\NT{binding-term}
+\nlsep \NT{elim-kw} ~\NT{binding-term}
+\nlsep \NT{elim-kw} ~\NT{binding-term} ~\TERM{using} ~\NT{binding-term}
+\nlsep \TERM{Intros} ~\NT{intro-pattern}
+\SEPDEF
+\DEFNT{elim-kw}
+       \TERM{Elim} ~\mid~ \TERM{Case} ~\mid~ \TERM{Induction}
+       ~\mid~ \TERM{Destruct}
+\end{rulebox}
+\caption{Grammaire des tactiques}
+\label{tactic}
+\end{figure}
+
+
+\subsection{Arguments de tactiques}
+
+La syntaxe actuelle des arguments de tactiques est que l'on parse par
+défaut une expression de tactique, ou bien l'on parse un terme si
+celui-ci est préfixé par \TERM{'} (sauf dans le cas des
+variables). Cela est gênant pour les utilisateurs qui doivent écrire
+des \TERM{'} pour leurs tactiques.
+
+À mon avis, il n'est pas souhaitable pour l'utilisateur de l'obliger à
+marquer une différence entre les tactiques ``primitives'' (en fait
+``système'') et les tactiques définies par Ltac. En effet, on se
+dirige inévitablement vers une situation où il existera des librairies
+de tactiques et il va devenir difficile de savoir facilement s'il faut
+ou non mettre des \TERM{'}.
+
+
+
+\subsection{Bindings}
+
+Dans un premier temps, les ``bindings'' sont toujours considérés comme
+une construction du langage des tactiques, mais il est intéressant de
+prévoir l'extension de ce procédé aux termes, puisqu'il s'agit
+simplement de construire un n{\oe}ud d'application dans lequel on
+donne les arguments par nom ou par position, les autres restant à
+inférer. Le principal point est de trouver comment combiner de manière
+uniforme ce procédé avec les arguments implicites.
+
+Il est toutefois important de réfléchir dès maintenant à une syntaxe
+pour éviter de rechanger encore la syntaxe.
+
+Intégrer la notation \TERM{with} aux termes peut poser des problèmes
+puisque ce mot-clé est utilisé pour le filtrage: comment parser (en
+LL(1)) l'expression:
+\begin{verbatim}
+Cases x with y ...
+\end{verbatim}
+
+Soit on trouve un autre mot-clé, soit on joue avec les niveaus de
+priorité en obligeant a parenthéser le \TERM{with} des ``bindings'':
+\begin{verbatim}
+Cases (x with y) with (C z) => ...
+\end{verbatim}
+ce qui introduit un constructeur moralement équivalent à une
+application situé à une priorité totalement différente (les
+``bindings'' seraient au plus haut niveau alors que l'application est
+à un niveau bas).
+
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{binding-term}
+       \NT{constr} ~\TERM{with} ~\STAR{\NT{binding}}
+\SEPDEF
+\DEFNT{binding}
+       \NT{constr}
+\end{rulebox}
+\caption{Grammaire des bindings}
+\label{bindings}
+\end{figure}
+
+\subsection{Enregistrements}
+
+Il faudrait aménager la syntaxe des enregistrements dans l'optique
+d'avoir des enregistrements anonymes (termes de première classe), même
+si pour l'instant, on ne dispose que d'enregistrements définis a
+toplevel.
+
+Exemple de syntaxe pour les types d'enregistrements:
+\begin{verbatim}
+{ x1 : A1;
+  x2 : A2(x1);
+  _ : T;   (* Pas de projection disponible *)
+  y;       (* Type infere *)
+  ...      (* ; optionnel pour le dernier champ *)
+}
+\end{verbatim}
+
+Exemple de syntaxe pour le constructeur:
+\begin{verbatim}
+{ x1 = O;
+  x2 : A2(x1) = v1;
+  _ = v2;
+  ...
+}
+\end{verbatim}
+Quant aux dépendences, une convention pourrait être de considérer les
+champs non annotés par le type comme non dépendants.
+
+Plusieurs interrogations:
+\begin{itemize}
+\item l'ordre des champs doit-il être respecté ?
+  sinon, que faire pour les champs sans projection ?
+\item autorise-t-on \texttt{v1} a mentionner \texttt{x1} (comme dans
+  la définition d'un module), ce qui se comporterait comme si on avait
+  écrit \texttt{v1} à la place. Cela pourrait être une autre manière
+  de déclarer les dépendences
+\end{itemize}
+
+La notation pointée pour les projections pose un problème de parsing,
+sauf si l'on a une convention lexicale qui discrimine les noms de
+modules des projections et identificateurs: \texttt{x.y.z} peut être
+compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}.
+
+
+\section{Grammaire des termes}
+\label{constrsyntax}
+
+\subsection{Quelques principes}
+
+\begin{enumerate}
+\item Diminuer le nombre de niveaux de priorité en regroupant les
+  règles qui se ressemblent: infixes, préfixes, lieurs (constructions
+  ouvertes à droite), etc.
+\item Éviter de surcharger la signification d'un symbole (ex:
+  \verb+( )+ comme parenthésage et produit dans la V7).
+\item Faire en sorte que les membres gauches (motifs de Cases, lieurs
+  d'abstraction ou de produits) utilisent une syntaxe compatible avec
+  celle des membres droits (branches de Cases et corps de fonction).
+\end{enumerate}
+
+\subsection{Présentation de la grammaire}
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{paren-constr}
+       \NT{cast-constr}~\TERM{,}~\NT{paren-constr}     &\RNAME{pair}
+\nlsep \NT{cast-constr}
+\SEPDEF
+\DEFNT{cast-constr}
+       \NT{constr}~\TERM{\!\!:}~\NT{cast-constr}       &\RNAME{cast}
+\nlsep \NT{constr}
+\SEPDEF
+\DEFNT{constr}
+       \NT{appl-constr}~\NT{infix}~\NT{constr}      &\RNAME{infix}
+\nlsep \NT{prefix}~\NT{constr}                      &\RNAME{prefix}
+\nlsep \NT{constr}~\NT{postfix}                     &\RNAME{postfix}
+\nlsep \NT{appl-constr}
+\SEPDEF
+\DEFNT{appl-constr}
+       \NT{appl-constr}~\PLUS{\NT{appl-arg}}           &\RNAME{apply}
+\nlsep \TERM{@}~\NT{global}~\PLUS{\NT{simple-constr}}  &\RNAME{expl-apply}
+\nlsep \NT{simple-constr}
+\SEPDEF
+\DEFNT{appl-arg}
+       \TERM{@}~\NT{int}~\TERM{\!:=}~\NT{simple-constr}  &\RNAME{impl-arg}
+\nlsep \NT{simple-constr}
+\SEPDEF
+\DEFNT{simple-constr}
+       \NT{atomic-constr}
+\nlsep \TERM{(}~\NT{paren-constr}~\TERM{)}
+\nlsep \NT{match-constr}
+\nlsep \NT{fix-constr}
+%% \nlsep \TERM{<\!\!:ast\!\!:<}~\NT{ast}~\TERM{>\!>} &\RNAME{quotation}
+\end{rulebox}
+\caption{Grammaire des termes}
+\label{constr}
+\end{figure}
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{prefix}
+       \TERM{!}~\PLUS{\NT{binder}}~\TERM{.}~    &\RNAME{prod}
+\nlsep \TERM{fun} ~\PLUS{\NT{binder}} ~\TERM{$\Rightarrow$} &\RNAME{lambda}
+\nlsep \TERM{let}~\NT{ident}~\STAR{\NT{binder}} ~\TERM{=}~\NT{constr}
+        ~\TERM{in}  &\RNAME{let}
+%\nlsep \TERM{let (}~\NT{comma-ident-list}~\TERM{) =}~\NT{constr}
+%        ~\TERM{in}   &~~~\RNAME{let-case}
+\nlsep \TERM{if}~\NT{constr}~\TERM{then}~\NT{constr}~\TERM{else}
+      &\RNAME{if-case}
+\nlsep \TERM{eval}~\NT{red-fun}~\TERM{in}       &\RNAME{eval}
+\SEPDEF
+\DEFNT{infix}
+      \TERM{$\rightarrow$}                     & \RNAME{impl}
+\SEPDEF
+\DEFNT{atomic-constr}
+      \TERM{_}
+\nlsep \TERM{?}\NT{int}
+\nlsep \NT{sort}
+\nlsep \NT{global}
+\SEPDEF
+\DEFNT{binder}
+       \NT{ident}                              &\RNAME{infer}
+\nlsep \TERM{(}~\NT{ident}~\NT{type}~\TERM{)}  &\RNAME{binder}
+\SEPDEF
+\DEFNT{type}
+       \TERM{\!:}~\NT{constr}
+\nlsep \epsilon
+\end{rulebox}
+\caption{Grammaires annexes aux termes}
+\label{gram-annexes}
+\end{figure}
+
+La grammaire des termes (correspondant à l'état \texttt{barestate})
+est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate
+par rapport aux précédentes versions de Coq d'importants changements
+de priorité, le plus marquant étant celui de l'application qui se
+trouve désormais juste au dessus\footnote{La convention est de
+considérer les opérateurs moins lieurs comme ``au dessus'',
+c'est-à-dire ayant un niveau de priorité plus élévé (comme c'est le
+cas avec le niveau de la grammaire actuelle des termes).} des
+constructions fermées à gauche et à droite.
+
+La grammaire des noms globaux est la suivante:
+\begin{eqnarray*}
+\DEFNT{global}
+      \NT{ident}
+%% \nlsep \TERM{\$}\NT{ident}
+\nlsep \NT{ident}\TERM{.}\NT{global}
+\end{eqnarray*}
+
+Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont
+reconnues au niveau du lexer pour ne pas entrer en conflit avec le
+$\TERM{?}$ de l'existentielle.
+
+Les opérateurs infixes ou préfixes sont tous au même niveau de
+priorité du point de vue de Camlp4. La solution envisagée est de les
+gérer à la manière de Yacc, avec une pile (voir discussions plus
+bas). Ainsi, l'implication est un infixe normal; la quantification
+universelle et le let sont vus comme des opérateurs préfixes avec un
+niveau de priorité plus haut (i.e. moins lieur). Il subsiste des
+problèmes si l'on ne veut pas écrire de parenthèses dans:
+\begin{verbatim}
+ A -> (!x. B -> (let y = C in D))
+\end{verbatim}
+
+La solution proposée est d'analyser le membre droit d'un infixe de
+manière à autoriser les préfixes et les infixes de niveau inférieur,
+et d'exiger le parenthésage que pour les infixes de niveau supérieurs.
+
+En revanche, à l'affichage, certains membres droits seront plus
+lisibles s'ils n'utilisent pas cette astuce:
+\begin{verbatim}
+(fun x => x) = fun x => x
+\end{verbatim}
+
+La proposition est d'autoriser ce type d'écritures au parsing, mais
+l'afficheur écrit de manière standardisée en mettant quelques
+parenthèses superflues: $\TERM{=}$ serait symétrique alors que
+$\rightarrow$ appellerait l'afficheur de priorité élevée pour son
+sous-terme droit.
+
+Les priorités des opérateurs primitifs sont les suivantes (le signe
+$*$ signifie que pour le membre droit les opérateurs préfixes seront
+affichés sans parenthèses quel que soit leur priorité):
+$$
+\begin{array}{c|l}
+$symbole$ & $priorité$ \\
+\hline
+\TERM{!}      & 200\,R* \\
+\TERM{fun}    & 200\,R* \\
+\TERM{let}    & 200\,R* \\
+\TERM{if}     & 200\,R \\
+\TERM{eval}   & 200\,R \\
+\rightarrow   & 90\,R*
+\end{array}
+$$
+
+Il y a deux points d'entrée pour les termes: $\NT{constr}$ et
+$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi
+d'un séparateur particulier. Dans le cas où l'on veut une liste de
+termes séparés par un espace, il faut lire des $\NT{simple-constr}$.
+
+
+
+Les constructions $\TERM{fix}$ et $\TERM{cofix}$ (voir aussi
+figure~\ref{gram-fix}) sont fermées par end pour simplifier
+l'analyse. Sinon, une expression de point fixe peut être suivie par un
+\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le
+``dangling else'': dans
+\begin{verbatim}
+fix f1 x {x} = fix f2 y {y} = ... and ... in ...
+\end{verbatim}
+il faut définir une stratégie pour associer le \TERM{and} et le
+\TERM{in} au bon point fixe.
+
+Un autre avantage est de faire apparaitre que le \TERM{fix} est un
+constructeur de terme de première classe et pas un lieur:
+\begin{verbatim}
+fix f1 ... and f2 ...
+in f1 end x
+\end{verbatim}
+Les propositions précédentes laissaient \texttt{f1} et \texttt{x}
+accolés, ce qui est source de confusion lorsque l'on fait par exemple
+\texttt{Pattern (f1 x)}.
+
+Les corps de points fixes et co-points fixes sont identiques, bien que
+ces derniers n'aient pas d'information de décroissance. Cela
+fonctionne puisque l'annotation est optionnelle. Cela préfigure des
+cas où l'on arrive à inférer quel est l'argument qui décroit
+structurellement (en particulier dans le cas où il n'y a qu'un seul
+argument).
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{fix-expr}
+       \TERM{fix}~\NT{fix-decls}    ~\NT{fix-select} ~\TERM{end} &\RNAME{fix}
+\nlsep \TERM{cofix}~\NT{cofix-decls}~\NT{fix-select} ~\TERM{end} &\RNAME{cofix}
+\SEPDEF
+\DEFNT{fix-decls}
+       \NT{fix-decl}~\TERM{and}~\NT{fix-decls}
+\nlsep \NT{fix-decl}
+\SEPDEF
+\DEFNT{fix-decl}
+       \NT{ident}~\PLUS{\NT{binder}}~\NT{type}~\NT{annot}
+       ~\TERM{=}~\NT{constr}
+\SEPDEF
+\DEFNT{annot}
+       \TERM{\{}~\NT{ident}~\TERM{\}}
+\nlsep \epsilon
+\SEPDEF
+\DEFNT{fix-select}
+       \TERM{in}~\NT{ident}
+\nlsep \epsilon
+\end{rulebox}
+\caption{Grammaires annexes des points fixes}
+\label{gram-fix}
+\end{figure}
+
+La construction $\TERM{Case}$ peut-être considérée comme
+obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et
+simplement.
+
+\begin{figure}
+\begin{rulebox}
+\DEFNT{match-expr}
+       \TERM{match}~\NT{case-items}~\NT{case-type}~\TERM{with}~
+       \NT{branches}~\TERM{end}        &\RNAME{match}
+\nlsep \TERM{match}~\NT{case-items}~\TERM{with}~
+       \NT{branches}~\TERM{end}        &\RNAME{infer-match}
+%%\nlsep \TERM{case}~\NT{constr}~\NT{case-predicate}~\TERM{of}~
+%%      \STAR{\NT{constr}}~\TERM{end}   &\RNAME{case}
+\SEPDEF
+\DEFNT{case-items}
+       \NT{case-item} ~\TERM{\&} ~\NT{case-items}
+\nlsep \NT{case-item}
+\SEPDEF
+\DEFNT{case-item}
+       \NT{constr}~\NT{pred-pattern} &\RNAME{dep-case}
+\nlsep \NT{constr}                   &\RNAME{nodep-case}
+\SEPDEF
+\DEFNT{case-type}
+       \TERM{$\Rightarrow$}~\NT{constr}
+\nlsep \epsilon
+\SEPDEF
+\DEFNT{pred-pattern}
+       \TERM{as}~\NT{ident} ~\TERM{\!:}~\NT{constr}
+\SEPDEF
+\DEFNT{branches}
+       \TERM{|} ~\NT{patterns} ~\TERM{$\Rightarrow$}
+        ~\NT{constr} ~\NT{branches}
+\nlsep \epsilon
+\SEPDEF
+\DEFNT{patterns}
+       \NT{pattern} ~\TERM{\&} ~\NT{patterns}
+\nlsep \NT{pattern}
+\SEPDEF
+\DEFNT{pattern} ...
+\end{rulebox}
+\caption{Grammaires annexes du filtrage}
+\label{gram-match}
+\end{figure}
+
+De manière globale, l'introduction de définitions dans les termes se
+fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au
+niveau vernac. Il y avait un manque de cohérence dans la
+V6, puisque l'on utilisait $=$ pour le $\TERM{let}$ et $\!:=$ pour les
+points fixes et les commandes vernac.
+
+% OBSOLETE: lieurs multiples supprimes
+%On peut remarquer que $\NT{binder}$ est un sous-ensemble de
+%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant
+%que lieur, {\tt a} et {\tt b} sont tous deux contraints, alors qu'en
+%tant que terme, seul {\tt b} l'est. Cela qui signifie que l'objectif
+%de rendre compatibles les membres gauches et droits est {\it presque}
+%atteint.
+
+\subsection{Infixes}
+
+\subsubsection{Infixes extensibles}
+
+Le problème de savoir si la liste des symboles pouvant apparaître en
+infixe est fixée ou extensible par l'utilisateur reste à voir.
+
+Notons que la solution où les symboles infixes sont des
+identificateurs que l'on peut définir paraît difficilement praticable:
+par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais
+ternaire. Il semble plus simple de garder des déclarations infixes qui
+relient un symbole infixe à un terme avec deux ``trous''. Par exemple:
+
+$$\begin{array}{c|l}
+$infixe$ &  $identificateur$ \\
+\hline
+= & \texttt{Logic.eq _ ?1 ?2} \\
+== & \texttt{JohnMajor.eq _ ?1 _ ?2}
+\end{array}$$
+
+La syntaxe d'une déclaration d'infixe serait par exemple:
+\begin{verbatim}
+Infix "=" 50 := Logic.eq _ ?1 ?2;
+\end{verbatim}
+
+
+\subsubsection{Gestion des précédences}
+
+Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici)
+considérer que tous les opérateurs ont la même précédence et gérer
+soit même la recomposition des termes à l'aide d'une pile (comme
+Yacc).
+
+
+\subsection{Extensions de syntaxe}
+
+\subsubsection{Litéraux numériques}
+
+La proposition est de considerer les litéraux numériques comme de
+simples identificateurs. Comme il en existe une infinité, il faut un
+nouveau mécanisme pour leur associer une définition. Par exemple, en
+ce qui concerne \texttt{Arith}, la définition de $5$ serait
+$\texttt{S}~4$. Pour \texttt{ZArith}, $5$ serait $\texttt{xI}~2$.
+
+Comme les infixes, les constantes numériques peuvent être qualifiées
+pour indiquer dans quels module est le type que l'on veut
+référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et
+\texttt{ZArith} en \texttt{Z}): \verb+N.5+, \verb+Z.5+.
+
+\begin{eqnarray*}
+\EXTNT{global}
+      \NT{int}
+\end{eqnarray*}
+
+\subsubsection{Nouveaux lieurs}
+
+$$
+\begin{array}{rclr}
+\EXTNT{constr}
+       \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}  &\RNAME{ex}
+\nlsep \TERM{ex}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr}
+        &\RNAME{ex2}
+\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}  &\RNAME{exT}
+\nlsep \TERM{ext}~\PLUS{\NT{binder}}~\TERM{.}~\NT{constr}~\TERM{,}~\NT{constr}
+        &\RNAME{exT2}
+\end{array}
+$$
+
+Pour l'instant l'existentielle n'admet qu'une seule variable, ce qui
+oblige à écrire des cascades de $\TERM{ex}$.
+
+Pour parser les existentielles avec deux prédicats, on peut considérer
+\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en
+présence de cet infixe se transforme en \texttt{ex2}.
+
+\subsubsection{Nouveaux infixes}
+
+Précédences des opérateurs infixes (les plus grands associent moins fort):
+$$
+\begin{array}{l|l|c|l}
+$identificateur$      & $module$     & $infixe/préfixe$ & $précédence$ \\
+\hline
+\texttt{iff}          & $Logic$      & \longleftrightarrow & 100 \\
+\texttt{or}           & $Logic$      & \vee     & 80\, R \\
+\texttt{sum}          & $Datatypes$  & +        & 80\, R \\
+\texttt{and}          & $Logic$      & \wedge   & 70\, R \\
+\texttt{prod}         & $Datatypes$  & *        & 70\, R \\
+\texttt{not}          & $Logic$      & \tilde{} & 60\, L \\
+\texttt{eq _}         & $Logic$      & =        & 50 \\
+\texttt{eqT _}        & $Logic_Type$ & =        & 50 \\
+\texttt{identityT _}  & $Data_Type$  & =        & 50 \\
+\texttt{le}           & $Peano$      & $<=$     & 50 \\
+\texttt{lt}           & $Peano$      & $<$      & 50 \\
+\texttt{ge}           & $Peano$      & $>=$     & 50 \\
+\texttt{gt}           & $Peano$      & $>$      & 50 \\
+\texttt{Zle}          & $zarith_aux$   & $<=$   & 50 \\
+\texttt{Zlt}          & $zarith_aux$   & $<$    & 50 \\
+\texttt{Zge}          & $zarith_aux$   & $>=$   & 50 \\
+\texttt{Zgt}          & $zarith_aux$   & $>$    & 50 \\
+\texttt{Rle}          & $Rdefinitions$ & $<=$   & 50 \\
+\texttt{Rlt}          & $Rdefinitions$ & $<$    & 50 \\
+\texttt{Rge}          & $Rdefinitions$ & $>=$   & 50 \\
+\texttt{Rgt}          & $Rdefinitions$ & $>$    & 50 \\
+\texttt{plus}         & $Peano$        & +      & 40\,L \\
+\texttt{Zplus}        & $fast_integer$ & +      & 40\,L \\
+\texttt{Rplus}        & $Rdefinitions$ & +      & 40\,L \\
+\texttt{minus}        & $Minus$        & -      & 40\,L \\
+\texttt{Zminus}       & $zarith_aux$   & -      & 40\,L \\
+\texttt{Rminus}       & $Rdefinitions$ & -      & 40\,L \\
+\texttt{Zopp}         & $fast_integer$ & -      & 40\,L \\
+\texttt{Ropp}         & $Rdefinitions$ & -      & 40\,L \\
+\texttt{mult}         & $Peano$        & *      & 30\,L \\
+\texttt{Zmult}        & $fast_integer$ & *      & 30\,L \\
+\texttt{Rmult}        & $Rdefinitions$ & *      & 30\,L \\
+\texttt{Rdiv}         & $Rdefinitions$ & /      & 30\,L \\
+\texttt{pow}          & $Rfunctions$   & \hat   & 20\,L \\
+\texttt{fact}         & $Rfunctions$   & !      & 20\,L \\
+\end{array}
+$$
+
+Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci
+définit deux égalités, ou alors les mettre dans des modules différents.
+
+\subsection{Exemples}
+
+\begin{verbatim}
+Definition not (A:Prop) := A->False;
+Inductive eq (A:Set) (x:A) : A->Prop :=
+    refl_equal : eq A x x;
+Inductive ex (A:Set) (P:A->Prop) : Prop :=
+    ex_intro : !x. P x -> ex A P;
+Lemma not_all_ex_not : !(P:U->Prop). ~(!n. P n) -> ?n. ~ P n;
+Fixpoint plus n m : nat {struct n} :=
+  match n with
+    O     => m
+  | (S k) => S (plus k m)
+  end;
+\end{verbatim}
+
+\subsection{Questions ouvertes}
+
+Voici les points sur lesquels la discussion est particulièrement
+ouverte:
+\begin{itemize}
+\item choix d'autres symboles pour les quantificateurs \TERM{!} et
+  \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!}
+  pour la qunatification universelle, mais on choisirait quelquechose
+  comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop
+  de symétrie entre ces quantificateurs (l'un est primitif, l'autre
+  pas).
+\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc.
+\item la possibilité d'introduire plusieurs variables du même type est
+  pour l'instant supprimée au vu des problèmes de compatibilité de
+  syntaxe entre les membres gauches et membres droits. L'idée étant
+  que l'inference de type permet d'éviter le besoin de déclarer tous
+  les types.
+\end{itemize}
+
+\subsection{Autres extensions}
+
+\subsubsection{Lieur multiple}
+
+L'écriture de types en présence de polymorphisme est souvent assez
+pénible:
+\begin{verbatim}
+Check !(A:Set) (x:A) (B:Set) (y:B). P A x B y;
+\end{verbatim}
+
+On pourrait avoir des déclarations introduisant à la fois un type
+d'une certaine sorte et une variable de ce type:
+\begin{verbatim}
+Check !(x:A:Set) (y:B:Set). P A x B y;
+\end{verbatim}
+
+Noter que l'on aurait pu écrire:
+\begin{verbatim}
+Check !A x B y. P A (x:A:Set) B (y:B:Set);
+\end{verbatim}
+
+\section{Syntaxe des tactiques}
+
+\subsection{Questions diverses}
+
+Changer ``Pattern nl c ... nl c'' en ``Pattern [ nl ] c ... [ nl ] c''
+pour permettre des chiffres seuls dans la catégorie syntaxique des
+termes.
+
+Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ?
+
+Même problème pour l'entier de Specialize (ou virer Specialize ?) ?
+
+\subsection{Questions en suspens}
+
+\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur
+et en profondeur ? Quelle recherche par défaut ?
+
+\section*{Remarques pêle-mêle (HH)}
+
+Autoriser la syntaxe
+
+\begin{verbatim}
+Variable R (a : A) (b : B) : Prop.
+Hypotheses H (a : A) (b : B) : Prop; Y (u : U) : V.
+Variables H (a : A) (b : B), J (k : K) : nat; Z (v : V) : Set.
+\end{verbatim}
+
+Renommer eqT, refl_eqT, eqT_ind, eqT_rect, eqT_rec en eq, refl_equal, etc.
+Remplacer == en =.
+
+Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ??
+
+\section{Moulinette}
+
+\begin{itemize}
+
+\item Mettre \verb=/= et * au même niveau dans R.
+
+\item Changer la précédence du - unaire dans R.
+
+\item Ajouter Require Arith par necessite si Require ArithRing ou Require ZArithRing.
+
+\item Ajouter Require ZArith par necessite si Require ZArithRing ou Require Omega.
+
+\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et
+l'ajouter à côté des Require Ring.
+
+\item Remplacer "Check n" par "n:Check ..."
+
+\item Renommer Variable/Hypothesis hors section en Parameter/Axiom.
+
+\item Renommer les \verb=command0=, \verb=command1=, ... \verb=lcommand= etc en
+\verb=constr0=, \verb=constr1=, ... \verb=lconstr=.
+
+\item Remplacer les noms Coq.omega.Omega par Coq.Omega ...
+
+\item Remplacer AddPath par Add LoadPath (ou + court)
+
+\item Unify + and \{\}+\{\} and +\{\} using Prop $\leq$ Set ??
+
+\item Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments.
+
+\item La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire.
+
+\item Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets).
+
+\item Remplacer Save. par Qed.
+
+\item Remplacer \verb=Zmult_Zplus_distr= par \verb=Zmult_plus_distr_r=
+et \verb=Zmult_plus_distr= par \verb=Zmult_plus_distr_l=.
+
+\end{itemize}
+
+\end{document}
diff --git a/dev/doc/archive/notes-on-conversion.v b/dev/doc/archive/notes-on-conversion.v
new file mode 100644
index 0000000000..a78ecd181a
--- /dev/null
+++ b/dev/doc/archive/notes-on-conversion.v
@@ -0,0 +1,71 @@
+(**********************************************************************)
+(* 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 controlled *)
+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/archive/old_svn_branches.txt b/dev/doc/archive/old_svn_branches.txt
new file mode 100644
index 0000000000..ee56ee24e9
--- /dev/null
+++ b/dev/doc/archive/old_svn_branches.txt
@@ -0,0 +1,33 @@
+## During the migration to git, some old branches and tags have not been
+## converted to directly visible git branches or tags. They are still there
+## in the archive, their names on the gforge repository are in the 3rd
+## column below (e.g. remotes/V8-0-bugfix). After a git clone, they
+## could always be accessed by their git hashref (2nd column below).
+
+# SVN   # GIT   # Symbolic name on gforge repository
+
+r5      d2f789d remotes/tags/start
+r1714   0605b7c remotes/V7
+r2583   372f3f0 remotes/tags/modules-2-branching
+r2603   6e15d9a remotes/modules
+r2866   76a93fa remotes/tags/modules-2-before-grammar
+r2951   356f749 remotes/tags/before-modules
+r2952   8ee67df remotes/tags/modules-2-update
+r2956   fb11bd9 remotes/modules-2
+r3193   4d23172 remotes/mowgli
+r3194   c91e99b remotes/tags/mowgli-before-merge
+r3500   5078d29 remotes/mowgli2
+r3672   63b0886 remotes/V7-3-bugfix
+r5086   bdceb72 remotes/V7-4-bugfix
+r5731   a274456 remotes/recriture
+r9046   e19553c remotes/tags/trunk
+r9146   b38ce05 remotes/coq-diff-tool
+r9786   a05abf8 remotes/ProofIrrelevance
+r10294  fdf8871 remotes/InternalExtraction
+r10408  df97909 remotes/TypeClasses
+r10673  4e19bca remotes/bertot
+r11130  bfd1cb3 remotes/proofs
+r12282  a726b30 remotes/revised-theories
+r13855  bae3a8e remotes/native
+r14062  b77191b remotes/recdef
+r16421  9f4bfa8 remotes/V8-0-bugfix
diff --git a/dev/doc/archive/perf-analysis b/dev/doc/archive/perf-analysis
new file mode 100644
index 0000000000..ac54fa6f73
--- /dev/null
+++ b/dev/doc/archive/perf-analysis
@@ -0,0 +1,167 @@
+Performance analysis (trunk repository)
+---------------------------------------
+
+Jun 7, 2010: delayed re-typing of Ltac instances in matching
+  (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem)
+
+Jun 4, 2010: improvement in eauto and type classes inference by removing
+  systematic preparation of debugging pretty-printing streams (std_ppcmds)
+  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk;
+   -6% in HighSchoolGeometry)
+
+Apr 19, 2010: small improvement obtained by reducing evar instantiation 
+  from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert,
+  -2% AreaMethod, -15% in Ssreflect)
+
+Apr 17, 2010: small improvement obtained by not repeating unification
+  twice in auto (-2% in Compcert, -2% in Algebra)
+
+Feb 15, 2010: Global decrease due to unicode inefficiency repaired
+
+Jan 8, 2010: Global increase due to an inefficiency in unicode treatment
+
+Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to
+  exact (generally not significative but, e.g., +25% on Subst, +8% on
+  ZFC, +5% on AreaMethod)
+
+Oct 19, 2009: Change in modules (CoLoR +35%)
+
+Aug 9, 2009: new files added in AreaMethod
+
+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%, LinAlg: +7%,
+   DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%)
+
+Sep 26, 2006: new field [r9178-9181]
+  (QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it)
+
+  Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s)
+  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)
+
+Dec 28, 2005: size decrease
+  mainly due to Defined moved to Qed in FSets (reduction from 95M to 7Mo)
+
+Dec 1-14, 2005: benchmarking server down
+  between the two dates: Godel: -10%, CoRN: -10%
+  probably due to changes around vm (new informative Cast,
+  change of equality in named_context_val) 
+
+  Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 25s)
+
+Aug 19, 2005: time decrease after application of "Array.length x=0" Xavier's 
+  suggestions for optimisation
+  (e.g. Nijmegen/QArith: -3%, Nijmegen/CoRN: -7%, Godel: -3%)
+ 
+  Aug 1, 2005: contrib Kildall added (~ 65s)
+
+Jul 26-Aug 2, 2005: bench down
+
+Jul 14-15, 2005: 4 contribs failed including CoRN
+
+Jul 14, 2005: time increase after activation of "closure optimisation"
+  (e.g. Nijmegen/QArith: +8%, Nijmegen/CoRN: +3%, Godel: +13%)
+
+  Jul 7, 2005: adding contrib Fermat4
+
+  Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 30s)
+
+  May 19, 2005: contrib Goodstein and prfx (~ 9s) added 
+
+Apr 21, 2005: strange time decrease
+  (could it be due to the change of Back and Reset mechanism) 
+  (e.g. Nijmegen/CoRN: -2%, Nijmegen/QARITH: -4%, Godel: -11%)
+
+Mar 20, 2005: fixed Logic.with_check bug
+  global time decrease (e.g. Nijmegen/CoRN: -3%, Nijmegen/QARITH: -1.5%)
+
+Jan 31-Feb 8, 2005: small instability
+  (e.g. CoRN: ~2015s -> ~1999s -> ~2032s, Godel: ~340s -> ~370s)
+
+  Jan 13, 2005: contrib SumOfTwoSquare added (~ 38s)
diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex
new file mode 100644
index 0000000000..25dabad497
--- /dev/null
+++ b/dev/doc/archive/versions-history.tex
@@ -0,0 +1,451 @@
+\documentclass[a4paper]{book}
+\usepackage{fullpage}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{amsfonts}
+
+\newcommand{\feature}[1]{{\em #1}}
+
+\begin{document}
+
+\begin{center}
+\begin{huge}
+A history of Coq versions
+\end{huge}
+\end{center}
+\bigskip
+
+\centerline{\large 1984-1989: The Calculus of Constructions}
+
+\bigskip
+\centerline{\large (see README.V1-V5 for details)}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+
+CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\
+         & 1984 to 13 February 1985 & \feature{of Constructions}, implementation  \\
+         & frozen 22 December 1984 & language is a predecessor of CAML\\
+
+CONSTR V1.11& mention of dates from 6 December\\
+         & 1984 to 19 February 1985 (freeze date) &\\
+
+CoC V2.8& dated 16 December 1985 (freeze date)\\
+
+CoC V2.9& & \feature{cumulative hierarchy of universes}\\
+
+CoC V2.13& dated 25 June 1986 (freeze date)\\
+
+CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\
+  & dated 20 November 1986 & implementation language now named CAML\\
+
+CoC V3.2& dated 27 November 1986\\
+
+CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\
+
+CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\
+
+CoC V4.1& dated 24 July 1987 (freeze date)\\
+
+CoC V4.2& dated 10 September 1987\\
+
+CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\
+  & frozen November 1987 & \feature{section mechanism}\\
+  & & \feature{logical vs computational content (sorte Spec)}\\
+  & & \feature{LCF engine}\\
+
+CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\
+  & frozen March 1988\\
+
+CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\
+  & demonstrated in June 1988\\
+
+CoC V4.6& dated 1 September 1988 & start of LEGO fork\\
+
+CoC V4.7& started 6 September 1988 \\
+
+CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\
+
+CoC V4.8.5& dated 1 February 1989 & \\
+
+CoC V4.9& dated 1 March 1989 (release date)\\
+
+CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\
+\end{tabular}
+
+\bigskip
+
+\noindent Note: CoC above stands as an abbreviation for {\em Calculus of
+  Constructions}, official name of the system.
+\bigskip
+\bigskip
+
+\newpage
+
+\centerline{\large 1989-now: The Calculus of Inductive Constructions}
+\mbox{}\\
+\centerline{I- RCS archives in Caml and Caml-Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq V5.0 & headers dated 1 January 1990 & internal use \\
+  & & \feature{inductive types with primitive recursor}\\
+
+Coq V5.1 & ended 12 July 1990 & internal use \\
+
+Coq V5.2 & log dated 4 October 1990 & internal use \\
+
+Coq V5.3 & log dated 12 October 1990 & internal use \\
+
+Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\
+
+Coq V5.5 & started 6 December 1990 & internal use \\
+
+Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\
+ & & (in May at TYPES?)\\
+ & & \feature{rewrite tactic}\\
+ & & use of RCS at least from February 1991\\
+
+Coq V5.6& 7 August 1991 & \\
+
+Coq V5.6 patch 1& 13 November 1991 & \\
+
+Coq V5.6 (last) & mention of 27 November 1992\\
+
+Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\
+
+Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\
+
+& & has the xcoq graphical interface\\
+
+& & first explicit notion of standard library\\
+
+& & includes a MacOS 7-9 version\\
+
+Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\
+
+Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\
+
+Coq V5.8.3& released 6 December 1993 % Announce on coq-club
+          & with xcoq graphical interface and MacOS 7-9 support\\
+
+ & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\
+
+Coq V5.9 alpha& 7 July 1993 &
+experimental version based on evars refinement \\
+              & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\
+              & & version), not released\\
+
+& March 1994 & \feature{tauto} tactic in V5.9 branch\\
+
+Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\
+         & & not released\\
+\end{tabular}
+
+\bigskip
+\bigskip
+
+\footnotetext{archive lost?}
+
+\newpage
+
+\centerline{II- Starting with CVS archives in Caml-Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq V5.10 ``Murthy'' & 22 January 1994 &
+introduction of the ``DOPN'' structure\\
+ & & \feature{eapply/prolog} tactics\\
+ & & private use of cvs on madiran.inria.fr\\
+
+Coq V5.10.1 ``Murthy''& 15 April 1994 \\
+
+Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\
+
+Coq V5.10.3& 28 April 1994 \\
+
+Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\
+  & & \feature{type synthesis of hidden arguments}\\
+  & & \feature{separate compilation}, \feature{reset mechanism} \\
+
+Coq V5.10.6& dated 30 May 1994\\
+Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\
+
+Coq V5.10.9& announced on 17 August 1994 &
+ % Announced by Catherine Parent on coqdev
+ % Version avec une copie de THEORIES pour les inductifs mutuels
+ \\
+
+Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\
+Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\
+ & & with first dispatch of files over src/* directories\\
+
+Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\
+
+Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\
+
+Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\
+
+Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW
+
+Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
+  & & MS-DOS version released on 30 October 1995\\
+ % still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009
+ % also known in /net/pauillac/constr archive as ``V5.11 old'' \\
+ % A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is
+ % known in /net/pauillac/constr archive as ``V5.11 new old'' \\
+
+Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\
+  % Announce on coq-club by BW
+  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive
+  & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW
+
+Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\
+\end{tabular}
+
+\bigskip
+\bigskip
+
+\newpage
+
+\centerline{III- A CVS archive in Caml Special Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\
+ & & to Caml Special Light (to later become Objective Caml)\\
+ & & has implicit arguments and coercions\\
+ & & has coinductive types\\
+
+Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\
+ & & \feature{omega} [10-9-1996] \\
+ & & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\
+ & & \feature{pattern-matching compilation} [7-10-1996]\\
+ & & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\
+
+Coq V6.1& released December 1996 & \\
+
+Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP
+      \feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\
+  & & grammar extension mechanism moved to Camlp4 [12-6-1997]\\
+  & & \feature{refine tactic}\\
+  & & includes a Windows version\\
+
+Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP
+  \feature{ring} (version 2) [7-4-1998] \\
+
+Coq V6.2.1& released 23 July 1998\\
+
+Coq V6.2.2 beta& released 30 January 1998\\
+
+Coq V6.2.2& released 23 September 1998\\
+
+Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\
+
+Coq V6.2.4& released 8 February 1999\\
+
+Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\
+ & & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\
+
+Coq V6.3.1& released 7 December 1999\\
+\end{tabular}
+\medskip
+\bigskip
+
+\newpage
+\centerline{IV- New CVS, back to a kernel-centric implementation}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\
+   & & \feature{kernel-centric} architecture \\
+   & & more care for outside readers\\
+   & & (indentation, ocaml warning protection)\\
+Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\
+Coq V7.0beta2& released 2 February 2001\\
+
+Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
+  & & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\
+
+Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\
+
+Coq V7.2& released 10 January 2002\\
+
+Coq V7.3& released 16 May 2002\\
+
+Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\
+  & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\
+
+Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\
+\end{tabular}
+
+\medskip
+\bigskip
+
+\centerline{V- New concrete syntax}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\
+
+Coq V8.0pl1& released 18 July 2004\\
+
+Coq V8.0pl2& released 22 January 2005\\
+
+Coq V8.0pl3& released 13 January 2006\\
+
+Coq V8.0pl4& released 26 January 2007\\
+
+Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\
+
+Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\
+  & & \feature{setoid rewriting} (version 2) [3-9-2004]\\
+  & & \feature{functional induction} [1-2-2006]\\
+  & & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\
+  & & \feature{Program} (version 2, Russell) [5-3-2006] \\
+  & & \feature{declarative language} [20-9-2006]\\
+  & & \feature{ring} (version 3) [18-11-2005]\\
+
+Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\
+
+Coq V8.1& released 10 February 2007 & \\
+
+Coq V8.1pl1& released 27 July 2007 & \\
+Coq V8.1pl2& released 13 October 2007 & \\
+Coq V8.1pl3& released 13 December 2007 & \\
+Coq V8.1pl4& released 9 October 2008 & \\
+
+Coq V8.2 beta1& released 13 June 2008 & \\
+Coq V8.2 beta2& released 19 June 2008 & \\
+Coq V8.2 beta3& released 27 June 2008 & \\
+Coq V8.2 beta4& released 8 August 2008 & \\
+
+Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\
+  & & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\
+  & & \feature{setoid rewriting} (version 3) [18-12-2007] \\
+  & & \feature{micromega solving platform} [19-5-2008]\\
+
+& & a first package released on
+February 11 was incomplete\\
+Coq V8.2pl1& released 4 July 2009 & \\
+Coq V8.2pl2& released 29 June 2010 & \\
+\end{tabular}
+
+\medskip
+\bigskip
+
+\newpage
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\
+Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\
+Coq V8.3pl1& released 23 December 2010 & \\
+Coq V8.3pl2& released 19 April 2011 & \\
+Coq V8.3pl3& released 19 December 2011 & \\
+Coq V8.3pl3& released 26 March 2012 & \\
+Coq V8.3pl5& released 28 September 2012 & \\
+Coq V8.4 beta & released 27 December 2011 &  \feature{modular arithmetic library} [2010-2012]\\
+&& \feature{vector library} [10-12-2010]\\
+&& \feature{structured scripts} [22-4-2010]\\
+&& \feature{eta-conversion} [20-9-2010]\\
+&& \feature{new proof engine available} [10-12-2010]\\
+Coq V8.4 beta2 & released 21 May 2012 & \\
+Coq V8.4 & released 12 August 2012 &\\
+Coq V8.4pl1& released 22 December 2012 & \\
+Coq V8.4pl2& released 4 April 2013 & \\
+Coq V8.4pl3& released 21 December 2013 & \\
+Coq V8.4pl4& released 24 April 2014 & \\
+Coq V8.4pl5& released 22 October 2014 & \\
+Coq V8.4pl6& released 9 April 2015 & \\
+
+Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\
+&& \feature{asynchonous evaluation} [8-8-2013]\\
+&& \feature{new proof engine deployed} [2-11-2013]\\
+&& \feature{universe polymorphism} [6-5-2014]\\
+&& \feature{primitive projections} [6-5-2014]\\
+&& \feature{miscellaneous optimizations}\\
+
+Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\
+
+Coq V8.5 & released 22 January 2016 & \\
+
+Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\
+&& \feature{Ltac profiling} [14-6-2016]\\
+&& \feature{warning system} [29-6-2016]\\
+&& \feature{miscellaneous optimizations}\\
+
+Coq V8.6 & released 14 December 2016 & \\
+
+Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\
+&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\
+&& \feature{further optimizations}\\
+
+Coq V8.7 beta 2 & released 6 October 2017 & \\
+
+Coq V8.7.0 & released 18 October 2017 & \\
+
+Coq V8.7.1 & released 15 December 2017 & \\
+
+Coq V8.7.2 & released 17 February 2018 & \\
+
+Coq V8.8 beta1 & released 19 March 2018 & \\
+
+Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\
+&& \feature{effort towards better documented, better structured ML API}\\
+&& \feature{miscellaneous changes/improvements of existing features}\\
+
+\end{tabular}
+
+\medskip
+\bigskip
+\newpage
+
+\centerline{\large Other important dates}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Lechenadec's version in C& mention of \\
+ & 13 January 1985 on \\
+ & some vernacular files\\
+Set up of the coq-club mailing list & 28 July 1993\\
+
+Coq V6.0 ``evars'' & & experimentation based on evars
+refinement started \\
+  & & in 1991 by Gilles from V5.6 beta,\\
+  & & with work by Hugo in July 1992\\
+
+Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first
+evars-based experimentation \\
+ & & to Coq V5.7, version from October/November
+1992\\
+
+CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet
+
+Proto with explicit substitutions & 1997 &\\
+
+Coq web site & 15 April 1998 & new site designed by David Delahaye \\
+
+Coq web site & January 2004 & web site new style \\
+  & & designed by Julien Narboux and Florent Kirchner \\
+
+Coq web site & April 2009 & new Drupal-based site \\
+  & & designed by Jean-Marc Notin and Denis Cousineau \\
+
+\end{tabular}
+
+\end{document}