Merge branch 'master' into sphinx-doc-chapter-22

9 files changed, 1234 insertions, 1479 deletions

diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
deleted file mode 100644
index 8961b0096..000000000
--- a/doc/refman/CanonicalStructures.tex
+++ /dev/null
@@ -1,383 +0,0 @@
-\achapter{Canonical Structures}
-%HEVEA\cutname{canonical-structures.html}
-\aauthor{Assia Mahboubi and Enrico Tassi}
-
-\label{CS-full}
-\index{Canonical Structures!presentation}
-
-\noindent This chapter explains the basics of Canonical Structure and how they can be used
-to overload notations and build a hierarchy of algebraic structures.
-The examples are taken from~\cite{CSwcu}.  We invite the interested reader
-to refer to this paper for all the details that are omitted here for brevity.
-The interested reader shall also find in~\cite{CSlessadhoc} a detailed
-description of another, complementary, use of Canonical Structures:
-advanced proof search.  This latter papers also presents many techniques one
-can employ to tune the inference of Canonical Structures.
-
-\section{Notation overloading}
-
-We build an infix notation $==$ for a comparison predicate.  Such notation
-will be overloaded, and its meaning will depend on the types of the terms
-that are compared.
-
-\begin{coq_eval}
-Require Import Arith.
-\end{coq_eval}
-
-\begin{coq_example}
-Module EQ.
-  Record class (T : Type) := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ the_cmp) := e in the_cmp.
-  Check op.
-  Arguments op {e} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-    Notation "x == y" := (op x y) (at level 70).
-  End theory.
-End EQ.
-\end{coq_example}
-
-We use Coq modules as name spaces.  This allows us to follow the same pattern
-and naming convention for the rest of the chapter.  The base name space
-contains the definitions of the algebraic structure.  To keep the example
-small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
-and characterizes terms on which a binary relation is defined, without
-requiring such relation to validate any property.
-The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
-will eventually contain lemmas holding on all the instances of the
-algebraic structure (in this case there are no lemmas).
-
-Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
-but we will not do that here.
-
-The following line tests that, when we assume a type \texttt{e} that is in the
-\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
-
-\begin{coq_example}
-Import EQ.theory.
-Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
-\end{coq_example}
-
-Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
-with a comparison relation.
-
-\begin{coq_example}
-Fail Check 3 == 3.
-Definition nat_eq (x y : nat) := nat_compare x y = Eq.
-Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
-Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
-Check 3 == 3.
-Eval compute in 3 == 4.
-\end{coq_example}
-
-This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
-also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
-relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
-can be read in the line declaring the canonical structure \texttt{nat\_EQty},
-where the first argument to \texttt{Pack} is the key and its second argument
-a group of canonical values associated to the key.  In this case we associate
-to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
-member).  The use of the projection \texttt{op} requires its argument to be in
-the class \texttt{EQ}, and uses such a member (function) to actually compare
-its arguments.
-
-Similarly, we could equip any other type with a comparison relation, and
-use the \texttt{==} notation on terms of this type.
-
-\subsection{Derived Canonical Structures}
-
-We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
-Here we show how to deal with type constructors, i.e. how to make the
-following example work:
-
-\begin{coq_example}
-Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). 
-\end{coq_example}
-
-The error message is telling that Coq has no idea on how to compare
-pairs of objects.  The following construction is telling Coq exactly how to do
-that.
-
-\begin{coq_example}
-Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
-  fst x == fst y /\ snd x == snd y.
-Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
-Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
-  EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
-Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
-Check forall n m : nat, (3,4) == (n,m).
-\end{coq_example}
-
-Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
-relation for pairs whenever it is able to build a comparison relation
-for each component of the pair.  The declaration associates to the key
-\texttt{*} (the type constructor of pairs) the canonical comparison relation
-\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
-being themselves in the \texttt{EQ} class.
-
-\section{Hierarchy of structures}
-
-To get to an interesting example we need another base class to be available.
-We choose the class of types that are equipped with an order relation,
-to which we associate the infix \texttt{<=} notation.
-
-\begin{coq_example}
-Module LE.
-  Record class T := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ f) := e in f.
-  Arguments op {_} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-  Notation "x <= y" := (op x y) (at level 70).
-  End theory.
-End LE.
-\end{coq_example}
-
-As before we register a canonical \texttt{LE} class for \texttt{nat}.
-
-\begin{coq_example}
-Import LE.theory.
-Definition nat_le x y := nat_compare x y <> Gt.
-Definition nat_LEcl : LE.class nat := LE.Class nat_le.
-Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
-\end{coq_example}
-
-And we enable Coq to relate pair of terms with \texttt{<=}.
-
-\begin{coq_example}
-Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
-  fst x <= fst y /\ snd x <= snd y.
-Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
-Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
-  LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
-Check (3,4,5) <= (3,4,5).
-\end{coq_example}
-
-At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
-like tuples of natural numbers, but we can't develop an algebraic
-theory over the types that are equipped with both relations.
-
-\begin{coq_example}
-Check 2 <= 3 /\ 2 == 2.
-Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
-Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
-\end{coq_example}
-
-We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
-
-\begin{coq_example}
-Module LEQ.
-  Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
-    Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
-  Record class T := Class {
-    EQ_class    : EQ.class T;
-    LE_class    : LE.class T;
-    extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
-  Structure type := _Pack { obj : Type; class_of : class obj }.
-  Arguments Mixin {e le} _.
-  Arguments Class {T} _ _ _.
-\end{coq_example}
-
-The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
-we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
-that the two relations we are combining are compatible.
-
-Unfortunately there is still an obstacle to developing the algebraic theory
-of this new class.
-
-\begin{coq_example}
-  Module theory.
-  Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
-\end{coq_example}
-
-The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
-a subclass relation.  In other words Coq does not see that an object
-of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
-
-The following two constructions tell Coq how to canonically build
-the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
-on the same type.
-
-\begin{coq_example}
-  Definition to_EQ (e : type) : EQ.type :=
-    EQ.Pack (obj e) (EQ_class _ (class_of e)).
-  Canonical Structure to_EQ.
-  Definition to_LE (e : type) : LE.type :=
-    LE.Pack (obj e) (LE_class _ (class_of e)).
-  Canonical Structure to_LE.
-\end{coq_example}
-We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
-\begin{coq_example}
-  Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
-   now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
-  Arguments lele_eq {e} x y _ _.
-  End theory.
-End LEQ.
-Import LEQ.theory.
-Check lele_eq.
-\end{coq_example}
-
-Of course one would like to apply results proved in the algebraic
-setting to any concrete instate of the algebraic structure.
-
-\begin{coq_example}
-Example test_algebraic (n m : nat) :  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-\end{coq_example}
-
-Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
-the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
-proofs are omitted for brevity.
-
-\begin{coq_example}
-Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-split.
-  unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-  case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ].
-  now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K.
-unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ].
-intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ].
-case (nat_compare_eq_iff m m); intros _ H1.
-now rewrite H1; auto; intro H2; discriminate H2.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
-Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-case n; case m; unfold EQ.op; unfold LE.op; simpl.
-intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ].
-  now split; apply lele_eq.
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1).
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2).
-intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4.
-now case H1; case H2; split; split.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
-\end{coq_example}
-
-The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
-type constructor \texttt{*}.  It also tests that they work as expected.
-
-Unfortunately, these declarations are very verbose.  In the following
-subsection we show how to make these declaration more compact.
-
-\begin{coq_example}
-Module Add_instance_attempt.
-  Canonical Structure nat_LEQty : LEQ.type :=
-    LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
-  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
-    LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
-      (LEQ.Class
-        (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
-        (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
-        (pair_LEQmx l1 l2)).
-  Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-  Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-End Add_instance_attempt.
-\end{coq_example}
-
-Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
-user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
-this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
-constructor preserves this property.  The combination of these two facts is a
-simple form of proof search that Coq performs automatically while inferring
-canonical structures.
-
-\subsection{Compact declaration of Canonical Structures}
-
-We need some infrastructure for that.
-
-\begin{coq_example*}
-Require Import Strings.String.
-\end{coq_example*}
-\begin{coq_example}
-Module infrastructure.
-  Inductive phantom {T : Type} (t : T) : Type := Phantom.
-  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
-    phantom t1 -> phantom t2.
-  Definition id {T} {t : T} (x : phantom t) := x.
-  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-    (at level 50, v ident, only parsing).
-  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-    (at level 50, v ident, only parsing).
-  Notation "'Error : t : s" := (unify _ t (Some s))
-    (at level 50, format "''Error'  :  t  :  s").
-  Open Scope string_scope.
-End infrastructure.
-\end{coq_example}
-
-To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one
-of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}.
-It should be read as: ``find a class e such that its objects have type T
-or fail with message "T is not an EQ.type"''.
-
-The other utilities are used to ask Coq to solve a specific unification
-problem, that will in turn require the inference of some canonical
-structures.  They are explained in mode details in~\cite{CSwcu}.
-
-We now have all we need to create a compact ``packager'' to declare
-instances of the \texttt{LEQ} class.
-
-\begin{coq_example}
-Import infrastructure.
-Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
-    [find e  | EQ.obj e ~ T       | "is not an EQ.type" ]
-    [find o  | LE.obj o ~ T       | "is not an LE.type" ]
-    [find ce | EQ.class_of e ~ ce ]
-    [find co | LE.class_of o ~ co ]
-    [find m  | m ~ m0             | "is not the right mixin" ]
-  LEQ._Pack T (LEQ.Class ce co m).
-Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
-\end{coq_example}
-
-The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
-the other pieces of the class \texttt{LEQ} and declares them as canonical values
-associated to the \texttt{T} key.  All in all, the only new piece of information
-we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
-for \texttt{T} and hence can be inferred by Coq.
-
-\texttt{Pack} is a notation, hence it is not type checked at the time of its
-declaration.  It will be type checked when it is used, an in that case
-\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
-pass to the 
-packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
-reader can refer to~\cite{CSwcu}. 
-
-The declaration of canonical instances can now be way more compact:
-
-\begin{coq_example}
-Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
-Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
-  Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
-\end{coq_example}
-
-Error messages are also quite intelligible (if one skips to the end of
-the message).
-
-\begin{coq_example}
-Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
-\end{coq_example}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
deleted file mode 100644
index 376ef031d..000000000
--- a/doc/refman/Cases.tex
+++ /dev/null
@@ -1,843 +0,0 @@
-\achapter{Extended pattern-matching}
-%HEVEA\cutname{cases.html}
-%BEGIN LATEX
-\defaultheaders
-%END LATEX
-\aauthor{Cristina Cornes and Hugo Herbelin}
-
-\label{Mult-match-full}
-\ttindex{Cases}
-\index{ML-like patterns}
-
-This section describes the full form of pattern-matching in {\Coq} terms.
-
-\asection{Patterns}\label{implementation} The full syntax of {\tt
-match} is presented in Figures~\ref{term-syntax}
-and~\ref{term-syntax-aux}.  Identifiers in patterns are either
-constructor names or variables. Any identifier that is not the
-constructor of an inductive or co-inductive type is considered to be a
-variable. A variable name cannot occur more than once in a given
-pattern. It is recommended to start variable names by a lowercase
-letter.
-
-If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor
-symbol and $\vec{x}$ is a linear vector of (distinct) variables, it is
-called {\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt match}. On the opposite, if it is a variable $x$ or
-has the form $(c~\vec{p})$ with $p$ not only made of variables, the
-pattern is called {\em nested}.
-
-A variable pattern matches any value, and the identifier is bound to
-that value. The pattern ``\texttt{\_}'' (called ``don't care'' or
-``wildcard'' symbol) also matches any value, but does not bind
-anything. It may occur an arbitrary number of times in a
-pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as}
-{\sl identifier}\texttt{)} are also accepted. This pattern matches the
-same values as {\sl pattern} does and {\sl identifier} is bound to the
-matched value.
-A pattern of the form {\pattern}{\tt |}{\pattern} is called
-disjunctive. A list of patterns separated with commas is also
-considered as a pattern and is called {\em multiple pattern}. However
-multiple patterns can only occur at the root of pattern-matching
-equations. Disjunctions of {\em multiple pattern} are allowed though.
-
-Since extended {\tt match} expressions are compiled into the primitive
-ones, the expressiveness of the theory remains the same. Once the
-stage of parsing has finished only simple patterns remain.  Re-nesting
-of pattern is performed at printing time. An easy way to see the
-result of the expansion is to toggle off the nesting performed at
-printing (use here {\tt Set Printing Matching}), then by printing the term
-with \texttt{Print} if the term is a constant, or using the command
-\texttt{Check}.
-
-The extended \texttt{match} still accepts an optional {\em elimination
-predicate} given after the keyword \texttt{return}.  Given a pattern
-matching expression, if all the right-hand-sides of \texttt{=>} ({\em
-rhs} in short) have the same type, then this type can be sometimes
-synthesized, and so we can omit the \texttt{return} part. Otherwise
-the predicate after \texttt{return} has to be provided, like for the basic
-\texttt{match}.
-
-Let us illustrate through examples the different aspects of extended
-pattern matching. Consider for example the function that computes the
-maximum of two natural numbers. We can write it in primitive syntax
-by:
-
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct m} : nat :=
-  match n with
-  | O => m
-  | S n' => match m with
-            | O => S n'
-            | S m' => S (max n' m')
-            end
-  end.
-\end{coq_example}
-
-\paragraph{Multiple patterns}
-
-Using multiple patterns in the definition of {\tt max} lets us write:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct m} : nat :=
-  match n, m with
-  | O, _ => m
-  | S n', O => S n'
-  | S n', S m' => S (max n' m')
-  end.
-\end{coq_example}
-
-which will be compiled into the previous form.
-
-The pattern-matching compilation strategy examines patterns from left
-to right. A \texttt{match} expression is generated {\bf only} when
-there is at least one constructor in the column of patterns. E.g. the
-following example does not build a \texttt{match} expression.
-
-\begin{coq_example}
-Check (fun x:nat => match x return nat with
-                    | y => y
-                    end).
-\end{coq_example}
-
-\paragraph{Aliasing subpatterns}
-
-We can also use ``\texttt{as} {\ident}'' to associate a name to a
-sub-pattern:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct n} : nat :=
-  match n, m with
-  | O, _ => m
-  | S n' as p, O => p
-  | S n', S m' => S (max n' m')
-  end.
-\end{coq_example}
-
-\paragraph{Nested patterns}
-
-Here is now an example of nested patterns:
-
-\begin{coq_example}
-Fixpoint even (n:nat) : bool :=
-  match n with
-  | O => true
-  | S O => false
-  | S (S n') => even n'
-  end.
-\end{coq_example}
-
-This is compiled into:
-
-\begin{coq_example}
-Unset Printing Matching.
-Print even.
-\end{coq_example}
-\begin{coq_eval}
-Set Printing Matching.
-\end{coq_eval}
-
-In the previous examples patterns do not conflict with, but
-sometimes it is comfortable to write patterns that admit a non
-trivial superposition. Consider
-the boolean function \texttt{lef} that given two natural numbers
-yields \texttt{true} if the first one is less or equal than the second
-one and \texttt{false} otherwise. We can write it as follows:
-
-\begin{coq_example}
-Fixpoint lef (n m:nat) {struct m} : bool :=
-  match n, m with
-  | O, x => true
-  | x, O => false
-  | S n, S m => lef n m
-  end.
-\end{coq_example}
-
-Note that the first and the second multiple pattern superpose because
-the couple of values \texttt{O O} matches both. Thus, what is the result
-of the function on those values?  To eliminate ambiguity we use the
-{\em textual priority rule}: we consider patterns ordered from top to
-bottom, then a value is matched by the pattern at the $ith$ row if and
-only if it is not matched by some pattern of a previous row. Thus in the
-example,
-\texttt{O O} is matched by the first pattern, and so \texttt{(lef O O)}
-yields \texttt{true}.
-
-Another way to write  this function is:
-
-\begin{coq_eval}
-Reset lef.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint lef (n m:nat) {struct m} : bool :=
-  match n, m with
-  | O, x => true
-  | S n, S m => lef n m
-  | _, _ => false
-  end.
-\end{coq_example}
-
-Here the last pattern superposes with the first two. Because
-of the priority rule, the last pattern
-will be used only for values that do not match neither the  first nor
-the second one.
-
-Terms with useless patterns are not accepted by the
-system. Here is an example:
-% Test failure: "This clause is redundant."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check (fun x:nat =>
-         match x with
-         | O => true
-         | S _ => false
-         | x => true
-         end).
-\end{coq_example}
-
-\paragraph{Disjunctive patterns}
-
-Multiple patterns that share the same right-hand-side can be
-factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
-{\tt max} can be rewritten as follows:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct m} : nat :=
-  match n, m with
-  | S n', S m' => S (max n' m')
-  | 0, p | p, 0 => p
-  end.
-\end{coq_example}
-
-Similarly, factorization of (non necessary multiple) patterns
-that share the same variables is possible by using the notation
-\nelist{\pattern}{\tt |}. Here is an example:
-
-\begin{coq_example}
-Definition filter_2_4 (n:nat) : nat :=
-  match n with
-  | 2 as m | 4 as m => m
-  | _ => 0
-  end.
-\end{coq_example}
-
-Here is another example using disjunctive subpatterns.
-
-\begin{coq_example}
-Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
-  match p with
-  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
-  | _ => (0,0)
-  end.
-\end{coq_example}
-
-\asection{About patterns of parametric types}
-\paragraph{Parameters in patterns}
-When matching objects of a parametric type, parameters do not bind in patterns.
-They must be substituted by ``\_''.
-Consider for example the type of polymorphic lists:
-
-\begin{coq_example}
-Inductive List (A:Set) : Set :=
-  | nil : List A
-  | cons : A -> List A -> List A.
-\end{coq_example}
-
-We can check the function {\em tail}:
-
-\begin{coq_example}
-Check
-  (fun l:List nat =>
-     match l with
-     | nil _ => nil nat
-     | cons _ _ l' => l'
-     end).
-\end{coq_example}
-
-
-When we use parameters in patterns there is an error message:
-% Test failure: "The parameters do not bind in patterns."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check
-  (fun l:List nat =>
-     match l with
-     | nil A => nil nat
-     | cons A _ l' => l'
-     end).
-\end{coq_example}
-
-The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
-(off by default) removes parameters from constructors in patterns:
-\begin{coq_example}
-  Set Asymmetric Patterns.
-  Check (fun l:List nat =>
-    match l with
-    | nil => nil
-    | cons _ l' => l'
-    end)
-  Unset Asymmetric Patterns.
-\end{coq_example}
-
-\paragraph{Implicit arguments in patterns}
-By default, implicit arguments are omitted in patterns. So we write:
-
-\begin{coq_example}
-Arguments nil [A].
-Arguments cons [A] _ _.
-Check
-  (fun l:List nat =>
-     match l with
-     | nil => nil
-     | cons _ l' => l'
-     end).
-\end{coq_example}
-
-But the possibility to use all the arguments is given by ``{\tt @}'' implicit
-explicitations (as for terms~\ref{Implicits-explicitation}).
-
-\begin{coq_example}
-Check
-  (fun l:List nat =>
-     match l with
-     | @nil _ => @nil nat
-     | @cons _ _ l' => l'
-     end).
-\end{coq_example}
-
-\asection{Matching objects of dependent types}
-The previous examples illustrate pattern matching on objects of
-non-dependent types, but we can also
-use the expansion strategy to destructure objects of dependent type.
-Consider the type \texttt{listn} of lists of a certain length:
-\label{listn}
-
-\begin{coq_example}
-Inductive listn : nat -> Set :=
-  | niln : listn 0
-  | consn : forall n:nat, nat -> listn n -> listn (S n).
-\end{coq_example}
-
-\asubsection{Understanding dependencies in patterns}
-We can define the function \texttt{length} over \texttt{listn} by:
-
-\begin{coq_example}
-Definition length (n:nat) (l:listn n) := n.
-\end{coq_example}
-
-Just for illustrating pattern matching,
-we can define it by case analysis:
-
-\begin{coq_eval}
-Reset length.
-\end{coq_eval}
-\begin{coq_example}
-Definition length (n:nat) (l:listn n) :=
-  match l with
-  | niln => 0
-  | consn n _ _ => S n
-  end.
-\end{coq_example}
-
-We can understand the meaning of this definition using the
-same notions of usual pattern matching.
-
-%
-% Constraining of dependencies is not longer valid in V7
-%
-\iffalse
-Now suppose we split the second pattern  of \texttt{length} into two
-cases so to give an
-alternative definition using nested patterns:
-\begin{coq_example}
-Definition length1 (n:nat) (l:listn n) :=
-  match l with
-  | niln => 0
-  | consn n _ niln => S n
-  | consn n _ (consn _ _ _) => S n
-  end.
-\end{coq_example}
-
-It is obvious that \texttt{length1} is  another version of
-\texttt{length}. We can also give the following definition:
-\begin{coq_example}
-Definition length2 (n:nat) (l:listn n) :=
-  match l with
-  | niln => 0
-  | consn n _ niln => 1
-  | consn n _ (consn m _ _) => S (S m)
-  end.
-\end{coq_example}
-
-If we forget that \texttt{listn} is a dependent type and we read these
-definitions using the usual semantics of pattern matching,  we can conclude
-that \texttt{length1}
-and \texttt{length2} are different functions.
-In fact, they are equivalent
-because the pattern \texttt{niln} implies that \texttt{n} can only match
-the value $0$ and analogously the pattern \texttt{consn} determines that \texttt{n} can
-only match  values of the form  $(S~v)$ where $v$ is the value matched by
-\texttt{m}.
-
-The converse is also true. If
-we destructure the  length  value with the pattern \texttt{O} then the list
-value should be $niln$.
-Thus, the following term \texttt{length3} corresponds to the function
-\texttt{length} but this time defined by case analysis on the dependencies instead of on the list:
-
-\begin{coq_example}
-Definition length3 (n:nat) (l:listn n) :=
-  match l with
-  | niln => 0
-  | consn O _ _ => 1
-  | consn (S n) _ _ => S (S n)
-  end.
-\end{coq_example}
-
-When we have nested patterns of dependent types, the semantics of
-pattern matching becomes a little more difficult because
-the set of values that are matched by a sub-pattern may be conditioned by the
-values matched by another sub-pattern. Dependent nested patterns are
-somehow constrained patterns.
-In the examples, the expansion of
-\texttt{length1} and \texttt{length2} yields exactly the same term
- but the
-expansion of \texttt{length3} is completely different. \texttt{length1} and
-\texttt{length2} are expanded into two nested case analysis on
-\texttt{listn} while \texttt{length3} is expanded into a case analysis on
-\texttt{listn} containing a case analysis on natural numbers inside.
-
-
-In practice the user can think about the patterns as independent and
-it is the expansion algorithm that cares to relate them. \\
-\fi
-%
-%
-%
-
-\asubsection{When the elimination predicate must be provided}
-\paragraph{Dependent pattern matching}
-The examples  given so far do not need an explicit elimination predicate
- because all the rhs have the same type and the
-strategy succeeds to synthesize it.
-Unfortunately when dealing with dependent patterns it often happens
-that we need to write cases where the type of the rhs are
-different  instances of the elimination  predicate.
-The function  \texttt{concat} for \texttt{listn}
-is an example where the branches have different type
-and we need to provide the elimination predicate:
-
-\begin{coq_example}
-Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
- listn (n + m) :=
-  match l in listn n return listn (n + m) with
-  | niln => l'
-  | consn n' a y => consn (n' + m) a (concat n' y m l')
-  end.
-\end{coq_example}
-The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}.
-In general if $m$ has type {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where
-$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of
-the form~:
-{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots}
-  $y_s${\tt ) =>} $Q$.
-
-In the concrete syntax, it should be written~:
-\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\ldots}~\kw{end}\]
-
-The variables which appear in the \kw{in} and \kw{as} clause are new
-and bounded in the property $Q$ in the \kw{return} clause. The
-parameters of the inductive definitions should not be mentioned and
-are replaced by \kw{\_}.
-
-\paragraph{Multiple dependent pattern matching}
-Recall that a list of patterns is also a pattern. So, when we destructure several
-terms at the same time and the branches have different types we need to provide the
-elimination predicate for this multiple pattern. It is done using the same
-scheme, each term may be associated to an \kw{as} and \kw{in} clause in order to
-introduce a dependent product.
-
-For example, an equivalent definition for \texttt{concat} (even though the
-matching on the second term is trivial) would have been:
-
-\begin{coq_eval}
-Reset concat.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
- listn (n + m) :=
-  match l in listn n, l' return listn (n + m) with
-  | niln, x => x
-  | consn n' a y, x => consn (n' + m) a (concat n' y m x)
-  end.
-\end{coq_example}
-
-Even without real matching over the second term, this construction can be used to
-keep types linked.  If {\tt a} and {\tt b} are two {\tt listn} of the same length,
-by writing
-\begin{coq_eval}
-  Unset Printing Matching.
-\end{coq_eval}
-\begin{coq_example}
-Check (fun n (a b: listn n) => match a,b with
- |niln,b0 => tt
- |consn n' a y, bS => tt
-end).
-\end{coq_example}
-\begin{coq_eval}
-  Set Printing Matching.
-\end{coq_eval}
-
-I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
-
-% Notice that this time, the predicate \texttt{[n,\_:nat](listn (plus n
-%   m))}  is binary because we
-% destructure both \texttt{l} and \texttt{l'} whose types have arity one.
-% In general, if we destructure the terms $e_1\ldots e_n$
-% the predicate will be of arity $m$ where $m$ is the sum of the
-% number of dependencies of the type of $e_1, e_2,\ldots e_n$
-% (the $\lambda$-abstractions
-% should correspond from left to right to each dependent argument of the
-% type of $e_1\ldots e_n$).
-% When the arity of the predicate (i.e. number of abstractions) is not
-% correct Coq raises an error message. For example:
-
-% % Test failure
-% \begin{coq_eval}
-% Reset concat.
-% Set Printing Depth 50.
-% (********** The following is not correct and should produce ***********)
-% (** Error: the term l' has type listn m while it is expected to have **)
-% (** type listn (?31 + ?32)                                           **)
-% \end{coq_eval}
-% \begin{coq_example}
-% Fixpoint concat
-%  (n:nat) (l:listn n) (m:nat)
-%  (l':listn m) {struct l} : listn (n + m) :=
-%   match l, l' with
-%   | niln, x => x
-%   | consn n' a y, x => consn (n' + m) a (concat n' y m x)
-%   end.
-% \end{coq_example}
-
-\paragraph{Patterns in {\tt in}}
-\label{match-in-patterns}
-
-If the type of the matched term is more precise than an inductive applied to
-variables, arguments of the inductive in the {\tt in} branch can be more
-complicated patterns than a variable.
-
-Moreover, constructors whose type do not follow the same pattern will
-become impossible branches. In an impossible branch, you can answer
-anything but {\tt False\_rect unit} has the advantage to be subterm of
-anything. % ???
-
-To be concrete: the {\tt tail} function can be written:
-\begin{coq_example}
-Definition tail n (v: listn (S n)) :=
-  match v in listn (S m) return listn m with
-  | niln => False_rect unit
-  | consn n' a y => y
-  end.
-\end{coq_example}
-and {\tt tail n v} will be subterm of {\tt v}.
-
-\asection{Using pattern matching to write proofs}
-In all the previous examples the elimination predicate does not depend
-on the object(s) matched. But it may depend and the typical case
-is when we write a proof by induction or a function that yields an
-object of dependent type. An example of proof using \texttt{match} in
-given in Section~\ref{refine-example}.
-
-For example, we can write
-the function \texttt{buildlist} that given a natural number
-$n$ builds a list of length $n$ containing zeros as follows:
-
-\begin{coq_example}
-Fixpoint buildlist (n:nat) : listn n :=
-  match n return listn n with
-  | O => niln
-  | S n => consn n 0 (buildlist n)
-  end.
-\end{coq_example}
-
-We can also use multiple patterns.
-Consider the following definition of the predicate less-equal
-\texttt{Le}:
-
-\begin{coq_example}
-Inductive LE : nat -> nat -> Prop :=
-  | LEO : forall n:nat, LE 0 n
-  | LES : forall n m:nat, LE n m -> LE (S n) (S m).
-\end{coq_example}
-
-We can use multiple patterns to write  the proof of the lemma
- \texttt{forall (n m:nat), (LE n m)}\verb=\/=\texttt{(LE m n)}:
-
-\begin{coq_example}
-Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
-  match n, m return LE n m \/ LE m n with
-  | O, x => or_introl (LE x 0) (LEO x)
-  | x, O => or_intror (LE x 0) (LEO x)
-  | S n as n', S m as m' =>
-      match dec n m with
-      | or_introl h => or_introl (LE m' n') (LES n m h)
-      | or_intror h => or_intror (LE n' m') (LES m n h)
-      end
-  end.
-\end{coq_example}
-In the example of \texttt{dec},
-the first \texttt{match} is dependent while
-the second is not.
-
-% In general, consider the terms $e_1\ldots e_n$,
-% where  the type of $e_i$ is an instance of a family type
-% $\lb (\vec{d_i}:\vec{D_i}) \mto T_i$  ($1\leq i
-% \leq n$). Then, in expression \texttt{match}  $e_1,\ldots,
-% e_n$ \texttt{of} \ldots \texttt{end}, the
-% elimination predicate ${\cal P}$ should be of the form:
-% $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
-
-The user can also use \texttt{match} in combination with the tactic
-\texttt{refine} (see Section~\ref{refine}) to build incomplete proofs
-beginning with a \texttt{match} construction.
-
-\asection{Pattern-matching on inductive objects involving local
-definitions}
-
-If local definitions occur in the type of a constructor, then there are two ways
-to match on this constructor. Either the local definitions are skipped and
-matching is done only on the true arguments of the constructors, or the bindings
-for local definitions can also be caught in the matching.
-
-Example.
-
-\begin{coq_eval}
-Reset Initial.
-Require Import Arith.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive list : nat -> Set :=
-  | nil : list 0
-  | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)).
-\end{coq_example*}
-
-In the next example, the local definition is not caught.
-
-\begin{coq_example}
-Fixpoint length n (l:list n) {struct l} : nat :=
-  match l with
-  | nil => 0
-  | cons n l0 => S (length (2 * n) l0)
-  end.
-\end{coq_example}
-
-But in this example, it is.
-
-\begin{coq_example}
-Fixpoint length' n (l:list n) {struct l} : nat :=
-  match l with
-  | nil => 0
-  | @cons _ m l0 => S (length' m l0)
-  end.
-\end{coq_example}
-
-\Rem for a given matching clause, either none of the local definitions or all of
-them can be caught.
-
-\Rem you can only catch {\tt let} bindings in mode where you bind all variables and so you
-have to use @ syntax.
-
-\Rem this feature is incoherent with the fact that parameters cannot be caught and
-consequently is somehow hidden. For example, there is no mention of it in error messages.
-
-\asection{Pattern-matching and coercions}
-
-If a mismatch occurs between the expected type of a pattern and its
-actual type, a coercion made from constructors is sought. If such a
-coercion can be found, it is automatically inserted around the
-pattern.
-
-Example:
-
-\begin{coq_example}
-Inductive I : Set :=
-  | C1 : nat -> I
-  | C2 : I -> I.
-Coercion C1 : nat >-> I.
-Check (fun x => match x with
-                | C2 O => 0
-                | _ => 0
-                end).
-\end{coq_example}
-
-
-\asection{When does the expansion strategy fail ?}\label{limitations}
-The strategy works very like in ML languages when treating
-patterns of non-dependent type.
-But there are new cases of failure that are due to the presence of
-dependencies.
-
-The error messages of the current implementation may be sometimes
-confusing.  When the tactic fails because patterns are somehow
-incorrect then error messages refer to the initial expression. But the
-strategy may succeed to build an expression whose sub-expressions are
-well typed when the whole expression is not. In this situation the
-message makes reference to the expanded expression.  We encourage
-users, when they have patterns with the same outer constructor in
-different equations, to name the variable patterns in the same
-positions with the same name.
-E.g. to write {\small\texttt{(cons n O x) => e1}}
-and {\small\texttt{(cons n \_ x) => e2}} instead of
-{\small\texttt{(cons n O x) => e1}} and
-{\small\texttt{(cons n' \_ x') => e2}}.
-This helps to maintain certain name correspondence between the
-generated expression and the original.
-
-Here is a summary of the error messages corresponding to each situation:
-
-\begin{ErrMsgs}
-\item \sverb{The constructor } {\sl
-    ident} \sverb{ expects } {\sl num} \sverb{ arguments}
-
- \sverb{The variable } {\sl ident} \sverb{ is bound several times
-    in pattern } {\sl term}
-
- \sverb{Found a constructor of inductive type } {\term}
- \sverb{ while a constructor of } {\term} \sverb{ is expected}
-
- Patterns are incorrect (because constructors are not applied to
-  the correct number of the arguments, because they are not linear or
-  they are wrongly typed).
-
-\item \errindex{Non exhaustive pattern-matching}
-
-The pattern matching is not exhaustive.
-
-\item \sverb{The elimination predicate } {\sl term} \sverb{ should be
-    of arity } {\sl num} \sverb{ (for non dependent case) or } {\sl
-    num} \sverb{ (for dependent case)}
-
-The elimination predicate provided to \texttt{match} has not the
-  expected arity.
-
-
-%\item the whole expression is wrongly typed
-
-% CADUC ?
-% , or the synthesis of
-%   implicit arguments fails (for example to find the elimination
-%   predicate or to resolve implicit arguments in the rhs).
-
-%   There are {\em nested patterns of dependent type}, the elimination
-%   predicate corresponds to non-dependent case and has the form
-%   $[x_1:T_1]...[x_n:T_n]T$ and {\bf some} $x_i$ occurs {\bf free} in
-%   $T$.  Then, the strategy may fail to find out a correct elimination
-%   predicate during some step of compilation.  In this situation we
-%   recommend the user to rewrite the nested dependent patterns into
-%   several \texttt{match} with {\em simple patterns}.
-
-\item {\tt Unable to infer a match predicate\\
-    Either there is a type incompatibility or the problem involves\\
-    dependencies}
-
-  There is a type mismatch between the different branches.
-  The user should provide an elimination predicate.
-
-% Obsolete ?
-% \item because of nested patterns, it may happen that even though all
-%   the rhs have the same type, the strategy needs dependent elimination
-%   and so an elimination predicate must be provided. The system warns
-%   about this situation, trying to compile anyway with the
-%   non-dependent strategy. The risen message is:
-
-% \begin{itemize}
-% \item {\tt Warning: This pattern matching may need dependent
-%     elimination to be compiled.  I will try, but if fails try again
-%     giving dependent elimination predicate.}
-% \end{itemize}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% % LA PROPAGATION DES CONTRAINTES ARRIERE N'EST PAS FAITE DANS LA V7
-% TODO
-% \item there are {\em nested patterns of dependent type} and the
-%   strategy builds a term that is well typed but recursive calls in fix
-%   point are reported as illegal:
-% \begin{itemize}
-% \item {\tt Error: Recursive call applied to an illegal term ...}
-% \end{itemize}
-
-% This is because the strategy generates a term that is correct w.r.t.
-% the initial term but which does not pass the guard condition.  In
-% this situation we recommend the user to transform the nested dependent
-% patterns into {\em several \texttt{match} of simple patterns}.  Let us
-% explain this with an example.  Consider the following definition of a
-% function that yields the last element of a list and \texttt{O} if it is
-% empty:
-
-% \begin{coq_example}
-%   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%    match l of
-%      (consn _ a niln) => a
-%    | (consn m _ x) => (last m x) | niln => O
-%    end.
-% \end{coq_example}
-
-% It fails because of the priority between patterns, we know that this
-% definition is equivalent to the following more explicit one (which
-% fails too):
-
-% \begin{coq_example*}
-%   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%    match l of
-%      (consn _ a niln) => a
-%    | (consn n _ (consn m b x)) => (last n (consn m b x))
-%    | niln => O
-%    end.
-% \end{coq_example*}
-
-% Note that the recursive call {\tt (last n (consn m b x))} is not
-% guarded. When treating with patterns of dependent types the strategy
-% interprets the first definition of \texttt{last} as the second
-% one\footnote{In languages of the ML family the first definition would
-%   be translated into a term where the variable \texttt{x} is shared in
-%   the expression.  When patterns are of non-dependent types, Coq
-%   compiles as in ML languages using sharing. When patterns are of
-%   dependent types the compilation reconstructs the term as in the
-%   second definition of \texttt{last} so to ensure the result of
-%   expansion is well typed.}.  Thus it generates a term where the
-% recursive call is rejected by the guard condition.
-
-% You can get rid of this problem by writing the definition with
-% \emph{simple patterns}:
-
-% \begin{coq_example}
-%   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%   <[_:nat]nat>match l of
-%     (consn m a x) => Cases x of niln => a | _ => (last m x) end
-%   | niln => O
-%   end.
-% \end{coq_example}
-
-\end{ErrMsgs}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End:
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
deleted file mode 100644
index 82765da6e..000000000
--- a/doc/refman/Omega.tex
+++ /dev/null
@@ -1,249 +0,0 @@
-\achapter{Omega: a solver of quantifier-free problems in
-Presburger Arithmetic}
-%HEVEA\cutname{omega.html}
-\aauthor{Pierre Crégut}
-\label{OmegaChapter}
-
-\asection{Description of {\tt omega}}
-\tacindex{omega}
-\label{description}
-
-{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
-quantified formula made of equations and inequations. Equations may
-be specified either on the type \verb=nat= of natural numbers or on
-the type \verb=Z= of binary-encoded integer numbers. Formulas on
-\verb=nat= are automatically injected into \verb=Z=.  The procedure
-may use any hypothesis of the current proof session to solve the goal.
-
-Multiplication is handled by {\tt omega} but only goals where at
-least one of the two multiplicands of products is a constant are
-solvable. This is the restriction meant by ``Presburger arithmetic''.
-
-If the tactic cannot solve the goal, it fails with an error message.
-In any case, the computation eventually stops.
-
-\asubsection{Arithmetical goals recognized by {\tt omega}}
-
-{\tt omega} applied only to quantifier-free formulas built from the
-connectors
-
-\begin{quote}
-\verb=/\, \/, ~, ->=
-\end{quote}
-
-on atomic formulas. Atomic formulas are built from the predicates 
-
-\begin{quote}
-\verb!=, le, lt, gt, ge!
-\end{quote}
-
- on \verb=nat= or from the predicates
-
-\begin{quote}
-\verb!=, <, <=, >, >=!
-\end{quote}
-
- on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
-
-\begin{quote}
-\verb!plus, minus, mult, pred, S, O!
-\end{quote}
-
-and in expressions of type \verb=Z=, {\tt omega} recognizes 
-
-\begin{quote}
-\verb!+, -, *, Z.succ!, and constants.
-\end{quote}
-
-All expressions of type \verb=nat= or \verb=Z= not built on these
-operators are considered abstractly as if they
-were arbitrary variables of type \verb=nat= or \verb=Z=.
-
-\asubsection{Messages from {\tt omega}}
-\label{errors}
-
-When {\tt omega} does not solve the goal, one of the following errors
-is generated:
-
-\begin{ErrMsgs}
-
-\item \errindex{omega can't solve this system}
-
-  This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try {\tt intros} first; if it contains
-  existentials quantifiers too, {\tt omega} is not strong enough to solve your
-  goal). This may happen also if your goal contains arithmetical
-  operators unknown from {\tt omega}. Finally, your goal may be really
-  wrong!
-
-\item \errindex{omega: Not a quantifier-free goal}
-  
-  If your goal is universally quantified, you should first apply {\tt
-    intro} as many time as needed.
-
-\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
-
-\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
-  
-\item \errindex{omega: Can't solve a goal with proposition variables}
-
-\item \errindex{omega: Unrecognized proposition}
-
-\item \errindex{omega: Can't solve a goal with non-linear products}
-
-\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
-
-\end{ErrMsgs}
-
-%% This code is currently unplugged
-%% 
-% \asubsection{Control over the output}
-% There are some flags that can be set to get more information on the procedure
-
-% \begin{itemize}
-% \item \verb=Time= to get the time used by the procedure
-% \item \verb=System= to visualize the normalized systems.
-% \item \verb=Action= to visualize the actions performed by the OMEGA
-%      procedure (see \ref{technical}).
-% \end{itemize}
-
-% \comindex{Set omega Time}
-% \comindex{UnSet omega Time}
-% \comindex{Switch omega Time}
-% \comindex{Set omega System}
-% \comindex{UnSet omega System}
-% \comindex{Switch omega System}
-% \comindex{Set omega Action}
-% \comindex{UnSet omega Action}
-% \comindex{Switch omega Action}
-
-% Use {\tt Set omega {\rm\sl flag}} to set the flag
-% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
-% {\tt Switch omega {\rm\sl flag}} to toggle it.
-
-\section{Using {\tt omega}}
-
-The {\tt omega} tactic does not belong to the core system. It should be
-loaded by
-\begin{coq_example*}
-Require Import Omega.
-Open Scope Z_scope.
-\end{coq_example*}
-
-\example{}
-
-\begin{coq_example}
-Goal forall m n:Z, 1 + 2 * m <> 2 * n.
-intros; omega.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\example{}
-
-\begin{coq_example}
-Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
-intro; omega.
-\end{coq_example}
-
-% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
-
-\section{Options}
-
-\begin{quote}
-  \optindex{Stable Omega}
-  {\tt Unset Stable Omega}
-\end{quote}
-This deprecated option (on by default) is for compatibility with Coq
-pre 8.5. It resets internal name counters to make executions of
-{\tt omega} independent.
-
-\begin{quote}
-  \optindex{Omega UseLocalDefs}
-  {\tt Unset Omega UseLocalDefs}
-\end{quote}
-This option (on by default) allows {\tt omega} to use the bodies of
-local variables.
-
-\begin{quote}
-  \optindex{Omega System}
-  {\tt Set Omega System}
-  \optindex{Omega Action}
-  {\tt Set Omega Action}
-\end{quote}
-These two options (off by default) activate the printing of debug
-information.
-
-\asection{Technical data}
-\label{technical}
-
-\asubsection{Overview of the tactic}
-\begin{itemize}
-
-\item The goal is negated twice and the first negation is introduced as an
-     hypothesis.
-\item Hypothesis are decomposed in simple equations or inequations. Multiple
-     goals may result from this phase.
-\item Equations and inequations over \verb=nat= are translated over
-     \verb=Z=, multiple goals may result from the translation of
-     substraction.
-\item Equations and inequations are normalized.
-\item Goals are solved by the {\it OMEGA} decision procedure.
-\item The script of the solution is replayed.
-
-\end{itemize}
-
-\asubsection{Overview of the {\it OMEGA} decision procedure}
-
-The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
-a small subset of the decision procedure presented in
-
-\begin{quote}
-  "The Omega Test: a fast and practical integer programming
-algorithm for dependence analysis", William Pugh, Communication of the
-ACM , 1992, p 102-114.
-\end{quote}
-
-Here is an overview, look at the original paper for more information.
-
-\begin{itemize}
-
-\item Equations and inequations are normalized by division by the GCD of their
-     coefficients.
-\item Equations are eliminated, using the Banerjee test to get a coefficient 
-     equal to one.
-\item Note that each inequation defines a half space in the space of real value
-     of the variables.
-   \item Inequations are solved by projecting on the hyperspace
-     defined by cancelling one of the variable.  They are partitioned
-     according to the sign of the coefficient of the eliminated
-     variable. Pairs of inequations from different classes define a
-     new edge in the projection.
-   \item Redundant inequations are eliminated or merged in new
-     equations that can be eliminated by the Banerjee test.
-\item The last two steps are iterated until a contradiction is reached
-     (success) or there is no more variable to eliminate (failure).
-
-\end{itemize}
-
-It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure (dark shadow) are not implemented, so the 
-decision procedure is only partial.
-
-\asection{Bugs}
-
-\begin{itemize}
-\item The simplification procedure is very dumb and this results in
-  many redundant cases to explore.
-
-\item Much too slow.
-
-\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}.
-
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4b7f9d91b..86f123322 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -117,11 +117,8 @@ Options A and B of the licence are {\em not} elected.}
 %END LATEX
 \part{Addendum to the Reference Manual}
 \include{AddRefMan-pre}%
-\include{Cases.v}%
 \include{Coercion.v}%
-\include{CanonicalStructures.v}%
 \include{Classes.v}%
-\include{Omega.v}%
 \include{Extraction.v}%
 \include{Program.v}%
 \include{Polynom.v}%  = Ring
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
new file mode 100644
index 000000000..6843e9eaa
--- /dev/null
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -0,0 +1,435 @@
+.. include:: ../replaces.rst
+.. _canonicalstructures:
+
+Canonical Structures
+======================
+
+:Authors: Assia Mahboubi and Enrico Tassi
+
+This chapter explains the basics of Canonical Structure and how they can be used
+to overload notations and build a hierarchy of algebraic structures. The
+examples are taken from :cite:`CSwcu`. We invite the interested reader to refer
+to this paper for all the details that are omitted here for brevity. The
+interested reader shall also find in :cite:`CSlessadhoc` a detailed description
+of another, complementary, use of Canonical Structures: advanced proof search.
+This latter papers also presents many techniques one can employ to tune the
+inference of Canonical Structures.
+
+
+Notation overloading
+-------------------------
+
+We build an infix notation == for a comparison predicate. Such
+notation will be overloaded, and its meaning will depend on the types
+of the terms that are compared.
+
+.. coqtop:: all
+  
+  Module EQ.
+    Record class (T : Type) := Class { cmp : T -> T -> Prop }.
+    Structure type := Pack { obj : Type; class_of : class obj }.
+    Definition op (e : type) : obj e -> obj e -> Prop :=
+      let 'Pack _ (Class _ the_cmp) := e in the_cmp.
+    Check op.
+    Arguments op {e} x y : simpl never.
+    Arguments Class {T} cmp.
+    Module theory.
+      Notation "x == y" := (op x y) (at level 70).
+    End theory.
+  End EQ.
+
+We use Coq modules as name spaces. This allows us to follow the same
+pattern and naming convention for the rest of the chapter. The base
+name space contains the definitions of the algebraic structure. To
+keep the example small, the algebraic structure ``EQ.type`` we are
+defining is very simplistic, and characterizes terms on which a binary
+relation is defined, without requiring such relation to validate any
+property. The inner theory module contains the overloaded notation ``==``
+and will eventually contain lemmas holding on all the instances of the
+algebraic structure (in this case there are no lemmas).
+
+Note that in practice the user may want to declare ``EQ.obj`` as a
+coercion, but we will not do that here.
+
+The following line tests that, when we assume a type ``e`` that is in
+theEQ class, then we can relates two of its objects with ``==``.
+
+.. coqtop:: all
+  
+  Import EQ.theory.
+  Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
+
+Still, no concrete type is in the ``EQ`` class.
+
+.. coqtop:: all
+
+  Fail Check 3 == 3.
+
+We amend that by equipping ``nat`` with a comparison relation.
+
+.. coqtop:: all
+  
+   Definition nat_eq (x y : nat) := Nat.compare x y = Eq.
+   Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
+   Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
+   Check 3 == 3.
+   Eval compute in 3 == 4.
+
+This last test shows that |Coq| is now not only able to typecheck ``3 == 3``,
+but also that the infix relation was bound to the ``nat_eq`` relation.
+This relation is selected whenever ``==`` is used on terms of type nat.
+This can be read in the line declaring the canonical structure
+``nat_EQty``, where the first argument to ``Pack`` is the key and its second
+argument a group of canonical values associated to the key. In this
+case we associate to nat only one canonical value (since its class,
+``nat_EQcl`` has just one member). The use of the projection ``op`` requires
+its argument to be in the class ``EQ``, and uses such a member (function)
+to actually compare its arguments.
+
+Similarly, we could equip any other type with a comparison relation,
+and use the ``==`` notation on terms of this type.
+
+
+Derived Canonical Structures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show
+how to deal with type constructors, i.e. how to make the following
+example work:
+
+
+.. coqtop:: all
+
+  Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
+
+The error message is telling that |Coq| has no idea on how to compare
+pairs of objects. The following construction is telling Coq exactly
+how to do that.
+
+.. coqtop:: all
+
+  Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
+    fst x == fst y /\ snd x == snd y.
+  
+  Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
+
+  Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
+      EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
+
+  Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
+
+  Check forall n m : nat, (3, 4) == (n, m).
+
+Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison
+relation for pairs whenever it is able to build a comparison relation
+for each component of the pair. The declaration associates to the key ``*``
+(the type constructor of pairs) the canonical comparison
+relation ``pair_eq`` whenever the type constructor ``*`` is applied to two
+types being themselves in the ``EQ`` class.
+
+Hierarchy of structures
+----------------------------
+
+To get to an interesting example we need another base class to be
+available. We choose the class of types that are equipped with an
+order relation, to which we associate the infix ``<=`` notation.
+
+.. coqtop:: all
+
+  Module LE.
+
+    Record class T := Class { cmp : T -> T -> Prop }.
+
+    Structure type := Pack { obj : Type; class_of : class obj }.
+
+    Definition op (e : type) : obj e -> obj e -> Prop :=
+      let 'Pack _ (Class _ f) := e in f.
+
+    Arguments op {_} x y : simpl never.
+
+    Arguments Class {T} cmp.
+  
+    Module theory.
+
+      Notation "x <= y" := (op x y) (at level 70).
+
+    End theory.
+
+  End LE.
+
+As before we register a canonical ``LE`` class for ``nat``.
+
+.. coqtop:: all
+
+  Import LE.theory.
+
+  Definition nat_le x y := Nat.compare x y <> Gt.
+
+  Definition nat_LEcl : LE.class nat := LE.Class nat_le.
+
+  Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
+
+And we enable |Coq| to relate pair of terms with ``<=``.
+
+.. coqtop:: all
+
+  Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
+     fst x <= fst y /\ snd x <= snd y.
+
+  Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
+
+  Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
+     LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
+
+  Check (3,4,5) <= (3,4,5).
+
+At the current stage we can use ``==`` and ``<=`` on concrete types, like
+tuples of natural numbers, but we can’t develop an algebraic theory
+over the types that are equipped with both relations.
+
+.. coqtop:: all
+
+  Check 2 <= 3 /\ 2 == 2.
+
+  Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
+
+  Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
+
+We need to define a new class that inherits from both ``EQ`` and ``LE``.
+
+
+.. coqtop:: all
+
+  Module LEQ.
+
+    Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
+      Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
+    
+    Record class T := Class {
+                        EQ_class : EQ.class T;
+                        LE_class : LE.class T;
+                        extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
+
+    Structure type := _Pack { obj : Type; class_of : class obj }.
+
+    Arguments Mixin {e le} _.
+
+    Arguments Class {T} _ _ _.
+
+The mixin component of the ``LEQ`` class contains all the extra content we
+are adding to ``EQ`` and ``LE``. In particular it contains the requirement
+that the two relations we are combining are compatible.
+
+Unfortunately there is still an obstacle to developing the algebraic
+theory of this new class.
+
+.. coqtop:: all
+
+    Module theory.
+
+    Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
+
+
+The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by
+a subclass relation. In other words |Coq| does not see that an object of
+the ``LEQ`` class is also an object of the ``LE`` class.
+
+The following two constructions tell |Coq| how to canonically build the
+``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same
+type.
+
+.. coqtop:: all
+
+    Definition to_EQ (e : type) : EQ.type :=
+       EQ.Pack (obj e) (EQ_class _ (class_of e)).
+
+    Canonical Structure to_EQ.
+
+    Definition to_LE (e : type) : LE.type :=
+       LE.Pack (obj e) (LE_class _ (class_of e)).
+ 
+    Canonical Structure to_LE.
+
+We can now formulate out first theorem on the objects of the ``LEQ``
+structure.
+
+.. coqtop:: all
+
+     Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
+
+     now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. 
+
+     Qed.
+
+     Arguments lele_eq {e} x y _ _.
+
+     End theory.
+
+  End LEQ.
+
+  Import LEQ.theory.
+
+  Check lele_eq.
+
+Of course one would like to apply results proved in the algebraic
+setting to any concrete instate of the algebraic structure.
+
+.. coqtop:: all
+
+  Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+
+  Fail apply (lele_eq n m). 
+
+  Abort.
+
+  Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+       n <= m -> m <= n -> n == m.
+
+  Fail apply (lele_eq n m). 
+
+  Abort.
+
+Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and
+how the type constructor ``*`` interacts with the ``LEQ`` class. In the
+following proofs are omitted for brevity.
+
+.. coqtop:: all
+
+  Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
+
+  Admitted.
+
+  Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
+
+  Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+     n <= m /\ m <= n <-> n == m.
+
+  Admitted.
+
+  Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
+
+The following script registers an ``LEQ`` class for ``nat`` and for the type
+constructor ``*``. It also tests that they work as expected.
+
+Unfortunately, these declarations are very verbose. In the following
+subsection we show how to make these declaration more compact.
+
+.. coqtop:: all
+
+  Module Add_instance_attempt.
+
+    Canonical Structure nat_LEQty : LEQ.type :=
+      LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
+
+    Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
+      LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
+        (LEQ.Class
+           (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
+           (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
+           (pair_LEQmx l1 l2)).
+
+     Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+
+     now apply (lele_eq n m). 
+
+     Qed.
+
+     Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
+
+     now apply (lele_eq n m). Qed.
+  
+  End Add_instance_attempt.
+
+Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by
+the user for ``n`` and m of type ``nat * nat``. What the user provides is a
+proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the
+pair constructor preserves this property. The combination of these two
+facts is a simple form of proof search that |Coq| performs automatically
+while inferring canonical structures.
+
+Compact declaration of Canonical Structures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We need some infrastructure for that.
+
+.. coqtop:: all
+
+  Require Import Strings.String.
+
+  Module infrastructure.
+
+    Inductive phantom {T : Type} (t : T) : Type := Phantom.
+
+    Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
+      phantom t1 -> phantom t2.
+
+    Definition id {T} {t : T} (x : phantom t) := x.
+
+    Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
+      (at level 50, v ident, only parsing).
+
+    Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
+      (at level 50, v ident, only parsing).
+
+    Notation "'Error : t : s" := (unify _ t (Some s))
+      (at level 50, format "''Error' : t : s").
+
+    Open Scope string_scope.
+
+  End infrastructure.
+
+To explain the notation ``[find v | t1 ~ t2]`` let us pick one of its
+instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be
+read as: “find a class e such that its objects have type T or fail
+with message "T is not an EQ.type"”.
+
+The other utilities are used to ask |Coq| to solve a specific unification
+problem, that will in turn require the inference of some canonical structures.
+They are explained in mode details in :cite:`CSwcu`.
+
+We now have all we need to create a compact “packager” to declare
+instances of the ``LEQ`` class.
+
+.. coqtop:: all
+
+  Import infrastructure.
+
+  Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
+    [find e | EQ.obj e ~ T | "is not an EQ.type" ]
+    [find o | LE.obj o ~ T | "is not an LE.type" ]
+    [find ce | EQ.class_of e ~ ce ]
+    [find co | LE.class_of o ~ co ]
+    [find m | m ~ m0 | "is not the right mixin" ]
+    LEQ._Pack T (LEQ.Class ce co m).
+
+   Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
+
+The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all
+the other pieces of the class ``LEQ`` and declares them as canonical
+values associated to the ``T`` key. All in all, the only new piece of
+information we add in the ``LEQ`` class is the mixin, all the rest is
+already canonical for ``T`` and hence can be inferred by |Coq|.
+
+``Pack`` is a notation, hence it is not type checked at the time of its
+declaration. It will be type checked when it is used, an in that case ``T`` is
+going to be a concrete type. The odd arguments ``_`` and ``id`` we pass to the
+packager represent respectively the classes to be inferred (like ``e``, ``o``,
+etc) and a token (``id``) to force their inference. Again, for all the details
+the reader can refer to :cite:`CSwcu`.
+
+The declaration of canonical instances can now be way more compact:
+
+.. coqtop:: all
+
+  Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
+  
+  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
+     Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
+
+Error messages are also quite intelligible (if one skips to the end of
+the message).
+
+.. coqtop:: all
+
+  Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
+
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
new file mode 100644
index 000000000..64d4eddf0
--- /dev/null
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -0,0 +1,611 @@
+.. include:: ../replaces.rst
+
+.. _extendedpatternmatching:
+
+Extended pattern-matching
+=========================
+
+:Authors: Cristina Cornes and Hugo Herbelin
+
+.. TODO links to figures
+
+This section describes the full form of pattern-matching in |Coq| terms.
+
+.. |rhs| replace:: right hand side
+
+Patterns
+--------
+
+The full syntax of match is presented in Figures 1.1 and 1.2.
+Identifiers in patterns are either constructor names or variables. Any
+identifier that is not the constructor of an inductive or co-inductive
+type is considered to be a variable. A variable name cannot occur more
+than once in a given pattern. It is recommended to start variable
+names by a lowercase letter.
+
+If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x
+is a linear vector of (distinct) variables, it is called *simple*: it
+is the kind of pattern recognized by the basic version of match. On
+the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not
+only made of variables, the pattern is called *nested*.
+
+A variable pattern matches any value, and the identifier is bound to
+that value. The pattern “``_``” (called “don't care” or “wildcard” symbol)
+also matches any value, but does not bind anything. It may occur an
+arbitrary number of times in a pattern. Alias patterns written
+:n:`(@pattern as @identifier)` are also accepted. This pattern matches the
+same values as ``pattern`` does and ``identifier`` is bound to the matched
+value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
+list of patterns separated with commas is also considered as a pattern
+and is called *multiple pattern*. However multiple patterns can only
+occur at the root of pattern-matching equations. Disjunctions of
+*multiple pattern* are allowed though.
+
+Since extended ``match`` expressions are compiled into the primitive ones,
+the expressiveness of the theory remains the same. Once the stage of
+parsing has finished only simple patterns remain. Re-nesting of
+pattern is performed at printing time. An easy way to see the result
+of the expansion is to toggle off the nesting performed at printing
+(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print`
+if the term is a constant, or using the command :cmd:`Check`.
+
+The extended ``match`` still accepts an optional *elimination predicate*
+given after the keyword ``return``. Given a pattern matching expression,
+if all the right-hand-sides of ``=>`` have the same
+type, then this type can be sometimes synthesized, and so we can omit
+the return part. Otherwise the predicate after return has to be
+provided, like for the basicmatch.
+
+Let us illustrate through examples the different aspects of extended
+pattern matching. Consider for example the function that computes the
+maximum of two natural numbers. We can write it in primitive syntax
+by:
+
+.. coqtop:: in undo
+
+   Fixpoint max (n m:nat) {struct m} : nat :=
+     match n with
+     | O => m
+     | S n' => match m with
+               | O => S n'
+               | S m' => S (max n' m')
+               end
+     end.
+
+Multiple patterns
+-----------------
+
+Using multiple patterns in the definition of max lets us write:
+
+.. coqtop:: in undo
+
+   Fixpoint max (n m:nat) {struct m} : nat :=
+       match n, m with
+       | O, _ => m
+       | S n', O => S n'
+       | S n', S m' => S (max n' m')
+       end.
+
+which will be compiled into the previous form.
+
+The pattern-matching compilation strategy examines patterns from left
+to right. A match expression is generated **only** when there is at least
+one constructor in the column of patterns. E.g. the following example
+does not build a match expression.
+
+.. coqtop:: all
+
+   Check (fun x:nat => match x return nat with
+                       | y => y
+                       end).
+
+
+Aliasing subpatterns
+--------------------
+
+We can also use :n:`as @ident` to associate a name to a sub-pattern:
+
+.. coqtop:: in undo
+
+   Fixpoint max (n m:nat) {struct n} : nat :=
+     match n, m with
+     | O, _ => m
+     | S n' as p, O => p
+     | S n', S m' => S (max n' m')
+     end.
+
+Nested patterns
+---------------
+
+Here is now an example of nested patterns:
+
+.. coqtop:: in
+
+   Fixpoint even (n:nat) : bool :=
+     match n with
+     | O => true
+     | S O => false
+     | S (S n') => even n'
+     end.
+
+This is compiled into:
+
+.. coqtop:: all undo
+
+   Unset Printing Matching.
+   Print even.
+
+In the previous examples patterns do not conflict with, but sometimes
+it is comfortable to write patterns that admit a non trivial
+superposition. Consider the boolean function :g:`lef` that given two
+natural numbers yields :g:`true` if the first one is less or equal than the
+second one and :g:`false` otherwise. We can write it as follows:
+
+.. coqtop:: in undo
+
+   Fixpoint lef (n m:nat) {struct m} : bool :=
+     match n, m with
+     | O, x => true
+     | x, O => false
+     | S n, S m => lef n m
+     end.
+
+Note that the first and the second multiple pattern superpose because
+the couple of values ``O O`` matches both. Thus, what is the result of the
+function on those values? To eliminate ambiguity we use the *textual
+priority rule*: we consider patterns ordered from top to bottom, then
+a value is matched by the pattern at the ith row if and only if it is
+not matched by some pattern of a previous row. Thus in the example,O O
+is matched by the first pattern, and so :g:`(lef O O)` yields true.
+
+Another way to write this function is:
+
+.. coqtop:: in
+
+   Fixpoint lef (n m:nat) {struct m} : bool :=
+     match n, m with
+     | O, x => true
+     | S n, S m => lef n m
+     | _, _ => false
+     end.
+
+Here the last pattern superposes with the first two. Because of the
+priority rule, the last pattern will be used only for values that do
+not match neither the first nor the second one.
+
+Terms with useless patterns are not accepted by the system. Here is an
+example:
+
+.. coqtop:: all
+
+   Fail Check (fun x:nat =>
+                 match x with
+                 | O => true
+                 | S _ => false
+                 | x => true
+                 end).
+
+
+Disjunctive patterns
+--------------------
+
+Multiple patterns that share the same right-hand-side can be
+factorized using the notation :n:`{+| @mult_pattern}`. For
+instance, :g:`max` can be rewritten as follows:
+
+.. coqtop:: in undo
+
+   Fixpoint max (n m:nat) {struct m} : nat :=
+     match n, m with
+     | S n', S m' => S (max n' m')
+     | 0, p | p, 0 => p
+     end.
+
+Similarly, factorization of (non necessary multiple) patterns that
+share the same variables is possible by using the notation :n:`{+| @pattern}`.
+Here is an example:
+
+.. coqtop:: in
+
+   Definition filter_2_4 (n:nat) : nat :=
+     match n with
+     | 2 as m | 4 as m => m
+     | _ => 0
+     end.
+
+
+Here is another example using disjunctive subpatterns.
+
+.. coqtop:: in
+
+   Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
+     match p with
+     | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
+     | _ => (0,0)
+     end.
+
+About patterns of parametric types
+----------------------------------
+
+Parameters in patterns
+~~~~~~~~~~~~~~~~~~~~~~
+
+When matching objects of a parametric type, parameters do not bind in
+patterns. They must be substituted by “``_``”. Consider for example the
+type of polymorphic lists:
+
+.. coqtop:: in
+
+   Inductive List (A:Set) : Set :=
+   | nil : List A
+   | cons : A -> List A -> List A.
+
+We can check the function *tail*:
+
+.. coqtop:: all
+
+   Check
+     (fun l:List nat =>
+        match l with
+        | nil _ => nil nat
+        | cons _ _ l' => l'
+        end).
+
+When we use parameters in patterns there is an error message:
+
+.. coqtop:: all
+
+   Fail Check
+     (fun l:List nat =>
+        match l with
+        | nil A => nil nat
+        | cons A _ l' => l'
+        end).
+
+.. opt:: Asymmetric Patterns
+
+This option (off by default) removes parameters from constructors in patterns:
+
+.. coqtop:: all
+
+   Set Asymmetric Patterns.
+   Check (fun l:List nat =>
+     match l with
+     | nil => nil
+     | cons _ l' => l'
+     end)
+   Unset Asymmetric Patterns.
+
+Implicit arguments in patterns
+------------------------------
+
+By default, implicit arguments are omitted in patterns. So we write:
+
+.. coqtop:: all
+
+   Arguments nil [A].
+   Arguments cons [A] _ _.
+   Check
+     (fun l:List nat =>
+        match l with
+        | nil => nil
+        | cons _ l' => l'
+        end).
+
+But the possibility to use all the arguments is given by “``@``” implicit
+explicitations (as for terms 2.7.11).
+
+.. coqtop:: all
+
+   Check
+     (fun l:List nat =>
+        match l with
+        | @nil _ => @nil nat
+        | @cons _ _ l' => l'
+        end).
+
+
+Matching objects of dependent types
+-----------------------------------
+
+The previous examples illustrate pattern matching on objects of non-
+dependent types, but we can also use the expansion strategy to
+destructure objects of dependent type. Consider the type :g:`listn` of
+lists of a certain length:
+
+.. coqtop:: in reset
+
+   Inductive listn : nat -> Set :=
+   | niln : listn 0
+   | consn : forall n:nat, nat -> listn n -> listn (S n).
+
+
+Understanding dependencies in patterns
+--------------------------------------
+
+We can define the function length over :g:`listn` by:
+
+.. coqtop:: in
+
+   Definition length (n:nat) (l:listn n) := n.
+
+Just for illustrating pattern matching, we can define it by case
+analysis:
+
+.. coqtop:: in
+
+   Definition length (n:nat) (l:listn n) :=
+     match l with
+     | niln => 0
+     | consn n _ _ => S n
+     end.
+
+We can understand the meaning of this definition using the same
+notions of usual pattern matching.
+
+
+When the elimination predicate must be provided
+-----------------------------------------------
+
+Dependent pattern matching
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The examples given so far do not need an explicit elimination
+predicate because all the |rhs| have the same type and the strategy
+succeeds to synthesize it. Unfortunately when dealing with dependent
+patterns it often happens that we need to write cases where the type
+of the |rhs| are different instances of the elimination predicate. The
+function concat for listn is an example where the branches have
+different type and we need to provide the elimination predicate:
+
+.. coqtop:: in
+
+   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+    listn (n + m) :=
+     match l in listn n return listn (n + m) with
+     | niln => l'
+     | consn n' a y => consn (n' + m) a (concat n' y m l')
+     end.
+
+The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`.
+In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr`
+are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`.
+
+In the concrete syntax, it should be written :
+``match m as x in (I _ … _ y1 … ys) return Q with … end``
+The variables which appear in the ``in`` and ``as`` clause are new and bounded
+in the property :g:`Q` in the return clause. The parameters of the
+inductive definitions should not be mentioned and are replaced by ``_``.
+
+Multiple dependent pattern matching
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Recall that a list of patterns is also a pattern. So, when we
+destructure several terms at the same time and the branches have
+different types we need to provide the elimination predicate for this
+multiple pattern. It is done using the same scheme, each term may be
+associated to an as and in clause in order to introduce a dependent
+product.
+
+For example, an equivalent definition for :g:`concat` (even though the
+matching on the second term is trivial) would have been:
+
+.. coqtop:: in
+
+   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+    listn (n + m) :=
+     match l in listn n, l' return listn (n + m) with
+     | niln, x => x
+     | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+     end.
+
+Even without real matching over the second term, this construction can
+be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same
+length, by writing
+
+.. coqtop:: in
+
+   Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+    listn (n + m) :=
+     match l in listn n, l' return listn (n + m) with
+     | niln, x => x
+     | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+     end.
+
+I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`.
+
+
+Patterns in ``in``
+~~~~~~~~~~~~~~~~~~
+
+If the type of the matched term is more precise than an inductive
+applied to variables, arguments of the inductive in the ``in`` branch can
+be more complicated patterns than a variable.
+
+Moreover, constructors whose type do not follow the same pattern will
+become impossible branches. In an impossible branch, you can answer
+anything but False_rect unit has the advantage to be subterm of
+anything.
+
+To be concrete: the tail function can be written:
+
+.. coqtop:: in
+
+   Definition tail n (v: listn (S n)) :=
+     match v in listn (S m) return listn m with
+     | niln => False_rect unit
+     | consn n' a y => y
+     end.
+
+and :g:`tail n v` will be subterm of :g:`v`.
+
+Using pattern matching to write proofs
+--------------------------------------
+
+In all the previous examples the elimination predicate does not depend
+on the object(s) matched. But it may depend and the typical case is
+when we write a proof by induction or a function that yields an object
+of dependent type. An example of proof using match in given in Section
+8.2.3.
+
+For example, we can write the function :g:`buildlist` that given a natural
+number :g:`n` builds a list of length :g:`n` containing zeros as follows:
+
+.. coqtop:: in
+
+   Fixpoint buildlist (n:nat) : listn n :=
+     match n return listn n with
+     | O => niln
+     | S n => consn n 0 (buildlist n)
+     end.
+
+We can also use multiple patterns. Consider the following definition
+of the predicate less-equal :g:`Le`:
+
+.. coqtop:: in
+
+   Inductive LE : nat -> nat -> Prop :=
+     | LEO : forall n:nat, LE 0 n
+     | LES : forall n m:nat, LE n m -> LE (S n) (S m).
+
+We can use multiple patterns to write the proof of the lemma
+:g:`forall (n m:nat), (LE n m) \/ (LE m n)`:
+
+.. coqtop:: in
+
+   Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
+     match n, m return LE n m \/ LE m n with
+     | O, x => or_introl (LE x 0) (LEO x)
+     | x, O => or_intror (LE x 0) (LEO x)
+     | S n as n', S m as m' =>
+         match dec n m with
+         | or_introl h => or_introl (LE m' n') (LES n m h)
+         | or_intror h => or_intror (LE n' m') (LES m n h)
+         end
+     end.
+
+In the example of :g:`dec`, the first match is dependent while the second
+is not.
+
+The user can also use match in combination with the tactic :tacn:`refine` (see
+Section 8.2.3) to build incomplete proofs beginning with a match
+construction.
+
+
+Pattern-matching on inductive objects involving local definitions
+-----------------------------------------------------------------
+
+If local definitions occur in the type of a constructor, then there
+are two ways to match on this constructor. Either the local
+definitions are skipped and matching is done only on the true
+arguments of the constructors, or the bindings for local definitions
+can also be caught in the matching.
+
+.. example::
+
+   .. coqtop:: in
+
+      Inductive list : nat -> Set :=
+      | nil : list 0
+      | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)).
+
+   In the next example, the local definition is not caught.
+
+   .. coqtop:: in
+
+      Fixpoint length n (l:list n) {struct l} : nat :=
+        match l with
+        | nil => 0
+        | cons n l0 => S (length (2 * n) l0)
+        end.
+
+   But in this example, it is.
+
+   .. coqtop:: in
+
+      Fixpoint length' n (l:list n) {struct l} : nat :=
+        match l with
+        | nil => 0
+        | @cons _ m l0 => S (length' m l0)
+        end.
+
+.. note:: For a given matching clause, either none of the local
+          definitions or all of them can be caught.
+
+.. note:: You can only catch let bindings in mode where you bind all
+          variables and so you have to use ``@`` syntax.
+
+.. note:: this feature is incoherent with the fact that parameters
+          cannot be caught and consequently is somehow hidden. For example,
+          there is no mention of it in error messages.
+
+Pattern-matching and coercions
+------------------------------
+
+If a mismatch occurs between the expected type of a pattern and its
+actual type, a coercion made from constructors is sought. If such a
+coercion can be found, it is automatically inserted around the
+pattern.
+
+.. example::
+
+   .. coqtop:: in
+
+      Inductive I : Set :=
+        | C1 : nat -> I
+        | C2 : I -> I.
+
+      Coercion C1 : nat >-> I.
+
+   .. coqtop:: all
+
+      Check (fun x => match x with
+                      | C2 O => 0
+                      | _ => 0
+                      end).
+
+
+When does the expansion strategy fail?
+--------------------------------------
+
+The strategy works very like in ML languages when treating patterns of
+non-dependent type. But there are new cases of failure that are due to
+the presence of dependencies.
+
+The error messages of the current implementation may be sometimes
+confusing. When the tactic fails because patterns are somehow
+incorrect then error messages refer to the initial expression. But the
+strategy may succeed to build an expression whose sub-expressions are
+well typed when the whole expression is not. In this situation the
+message makes reference to the expanded expression. We encourage
+users, when they have patterns with the same outer constructor in
+different equations, to name the variable patterns in the same
+positions with the same name. E.g. to write ``(cons n O x) => e1`` and
+``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and
+``(cons n' _ x') => e2``. This helps to maintain certain name correspondence between the
+generated expression and the original.
+
+Here is a summary of the error messages corresponding to each
+situation:
+
+.. exn:: The constructor @ident expects @num arguments
+
+   The variable ident is bound several times in pattern termFound a constructor
+   of inductive type term while a constructor of term is expectedPatterns are
+   incorrect (because constructors are not applied to the correct number of the
+   arguments, because they are not linear or they are wrongly typed).
+
+.. exn:: Non exhaustive pattern-matching
+
+   The pattern matching is not exhaustive.
+
+.. exn:: The elimination predicate term should be of arity @num (for non \
+         dependent case) or @num (for dependent case)
+
+   The elimination predicate provided to match has not the expected arity.
+
+.. exn:: Unable to infer a match predicate
+         Either there is a type incompatibility or the problem involves dependencies
+
+   There is a type mismatch between the different branches. The user should
+   provide an elimination predicate.
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
new file mode 100644
index 000000000..20e40c550
--- /dev/null
+++ b/doc/sphinx/addendum/omega.rst
@@ -0,0 +1,184 @@
+.. _omega:
+
+Omega: a solver for quantifier-free problems in Presburger Arithmetic
+=====================================================================
+
+:Author: Pierre Crégut
+
+Description of ``omega``
+------------------------
+
+This tactic does not need any parameter:
+
+.. tacn:: omega
+
+``omega`` solves a goal in Presburger arithmetic, i.e. a universally
+quantified formula made of equations and inequations. Equations may
+be specified either on the type ``nat`` of natural numbers or on
+the type ``Z`` of binary-encoded integer numbers. Formulas on
+``nat`` are automatically injected into ``Z``.  The procedure
+may use any hypothesis of the current proof session to solve the goal.
+
+Multiplication is handled by ``omega`` but only goals where at
+least one of the two multiplicands of products is a constant are
+solvable. This is the restriction meant by "Presburger arithmetic".
+
+If the tactic cannot solve the goal, it fails with an error message.
+In any case, the computation eventually stops.
+
+Arithmetical goals recognized by ``omega``
+------------------------------------------
+
+``omega`` applied only to quantifier-free formulas built from the
+connectors::
+
+   /\  \/  ~  ->
+
+on atomic formulas. Atomic formulas are built from the predicates::
+
+   =  <  <=  >  >=
+
+on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes::
+
+   +  -  *  S  O  pred
+
+and in expressions of type ``Z``, ``omega`` recognizes numeral constants and::
+
+   +  -  *  Z.succ Z.pred
+
+All expressions of type ``nat`` or ``Z`` not built on these
+operators are considered abstractly as if they
+were arbitrary variables of type ``nat`` or ``Z``.
+
+Messages from ``omega``
+-----------------------
+
+When ``omega`` does not solve the goal, one of the following errors
+is generated:
+
+.. exn:: omega can't solve this system
+
+  This may happen if your goal is not quantifier-free (if it is
+  universally quantified, try ``intros`` first; if it contains
+  existentials quantifiers too, ``omega`` is not strong enough to solve your
+  goal). This may happen also if your goal contains arithmetical
+  operators unknown from ``omega``. Finally, your goal may be really
+  wrong!
+
+.. exn:: omega: Not a quantifier-free goal
+
+  If your goal is universally quantified, you should first apply
+  ``intro`` as many time as needed.
+
+.. exn:: omega: Unrecognized predicate or connective: @ident
+
+.. exn:: omega: Unrecognized atomic proposition: ...
+
+.. exn:: omega: Can't solve a goal with proposition variables
+
+.. exn:: omega: Unrecognized proposition
+
+.. exn:: omega: Can't solve a goal with non-linear products
+
+.. exn:: omega: Can't solve a goal with equality on type ...
+
+
+Using ``omega``
+---------------
+
+The ``omega`` tactic does not belong to the core system. It should be
+loaded by
+
+.. coqtop:: in
+
+   Require Import Omega.
+
+.. example::
+
+  .. coqtop:: all
+
+     Require Import Omega.
+
+     Open Scope Z_scope.
+
+     Goal forall m n:Z, 1 + 2 * m <> 2 * n.
+     intros; omega.
+     Abort.
+
+     Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
+     intro; omega.
+     Abort.
+
+
+Options
+-------
+
+.. opt:: Stable Omega
+
+This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
+resets internal name counters to make executions of ``omega`` independent.
+
+.. opt:: Omega UseLocalDefs
+
+This option (on by default) allows ``omega`` to use the bodies of local
+variables.
+
+.. opt:: Omega System
+
+This option (off by default) activate the printing of debug information
+
+.. opt:: Omega Action
+
+This option (off by default) activate the printing of debug information
+
+Technical data
+--------------
+
+Overview of the tactic
+~~~~~~~~~~~~~~~~~~~~~~
+
+ * The goal is negated twice and the first negation is introduced as an hypothesis.
+ * Hypothesis are decomposed in simple equations or inequations. Multiple
+   goals may result from this phase.
+ * Equations and inequations over ``nat`` are translated over
+   ``Z``, multiple goals may result from the translation of substraction.
+ * Equations and inequations are normalized.
+ * Goals are solved by the OMEGA decision procedure.
+ * The script of the solution is replayed.
+
+Overview of the OMEGA decision procedure
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The OMEGA decision procedure involved in the ``omega`` tactic uses
+a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
+Here is an overview, look at the original paper for more information.
+
+ * Equations and inequations are normalized by division by the GCD of their
+   coefficients.
+ * Equations are eliminated, using the Banerjee test to get a coefficient
+   equal to one.
+ * Note that each inequation defines a half space in the space of real value
+   of the variables.
+ * Inequations are solved by projecting on the hyperspace
+   defined by cancelling one of the variable.  They are partitioned
+   according to the sign of the coefficient of the eliminated
+   variable. Pairs of inequations from different classes define a
+   new edge in the projection.
+ * Redundant inequations are eliminated or merged in new
+   equations that can be eliminated by the Banerjee test.
+ * The last two steps are iterated until a contradiction is reached
+   (success) or there is no more variable to eliminate (failure).
+
+It may happen that there is a real solution and no integer one. The last
+steps of the Omega procedure (dark shadow) are not implemented, so the
+decision procedure is only partial.
+
+Bugs
+----
+
+ * The simplification procedure is very dumb and this results in
+   many redundant cases to explore.
+
+ * Much too slow.
+
+ * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/.
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 4a9bd6c1a..247f32103 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -1312,7 +1312,7 @@ Languages},
   year        = {1994}
 }
 
-@article{ TheOmegaPaper,
+@article{TheOmegaPaper,
     author = "W. Pugh",
     title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
     journal = "Communication of the ACM",
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index ddcb4c4cb..c5d4936b1 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -43,6 +43,9 @@ Table of contents
 .. toctree::
    :caption: Addendum
 
+   addendum/extended-pattern-matching
+   addendum/canonical-structures
+   addendum/omega
    addendum/micromega
 
 .. toctree::