Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into multiple pages.

Reviewed-by: jfehrle

4 files changed, 47 insertions, 1055 deletions

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
deleted file mode 100644
index b593b0cef1..0000000000
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ /dev/null
@@ -1,437 +0,0 @@
-.. _canonicalstructures:
-
-Canonical Structures
-======================
-
-:Authors: Assia Mahboubi and Enrico Tassi
-
-This chapter explains the basics of canonical structures 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 namespaces. This allows us to follow the same
-pattern and naming convention for the rest of the chapter. The base
-namespace 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 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, we can relate 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 type check ``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; #[canonical(false)] 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.
-
-The `class_of` projection of the `type` structure is annotated as *not canonical*;
-it plays no role in the search for instances.
-
-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 them 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 more 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
deleted file mode 100644
index 8ec51e45ba..0000000000
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ /dev/null
@@ -1,617 +0,0 @@
-.. _extendedpatternmatching:
-
-Extended pattern matching
-=========================
-
-:Authors: Cristina Cornes and Hugo Herbelin
-
-This section describes the full form of pattern matching in |Coq| terms.
-
-.. |rhs| replace:: right hand sides
-
-Patterns
---------
-
-The full syntax of :g:`match` is presented in section :ref:`term`.
-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 @ident)` are also accepted. This pattern matches the
-same values as :token:`pattern` does and :token:`ident` 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 patterns* are allowed though.
-
-Since extended ``match`` expressions are compiled into the primitive ones,
-the expressiveness of the theory remains the same. Once parsing has finished
-only simple patterns remain. The original nesting of the ``match`` expressions
-is recovered at printing time. An easy way to see the result
-of the expansion is to toggle off the nesting performed at printing
-(use here :flag:`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
-
-   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 reset
-
-   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 reset
-
-   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
-
-   Unset Printing Matching.
-   Print even.
-
-.. coqtop:: none
-
-   Set Printing Matching.
-
-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
-
-   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 overlap 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 to be ordered from top to bottom. A
-value is matched by the pattern at the ith row if and only if it is
-not matched by some pattern from 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 reset
-
-   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:`{+| {+, @pattern } }`. For
-instance, :g:`max` can be rewritten as follows:
-
-.. coqtop:: in reset
-
-   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 (not necessarily 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.
-
-
-Nested disjunctive patterns are allowed, inside parentheses, with the
-notation :n:`({+| @pattern})`, as in:
-
-.. 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).
-
-.. flag:: Asymmetric Patterns
-
-   This flag (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, see :ref:`explicit-applications`).
-
-.. coqtop:: all
-
-   Check
-     (fun l:List nat =>
-        match l with
-        | @nil _ => @nil nat
-        | @cons _ _ l' => l'
-        end).
-
-
-.. _matching-dependent:
-
-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 types. 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:
-
-.. coqdoc::
-
-   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 Coq
-succeeds to synthesize it. Unfortunately when dealing with dependent
-patterns it often happens that we need to write cases where the types
-of the |rhs| are different instances of the elimination predicate. The
-function :g:`concat` for :g:`listn` is an example where the branches have
-different types 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.
-
-.. coqtop:: none
-
-   Reset concat.
-
-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`` clause and an ``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
-
-   Check (fun n (a b: listn n) =>
-    match a, b with
-    | niln, b0 => tt
-    | consn n' a y, bS => tt
-    end).
-
-we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`.
-
-.. _match-in-patterns:
-
-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 types 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 a dependent type. An example of a proof written using ``match`` is given
-in the description of the tactic :tacn:`refine`.
-
-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`
-to build incomplete proofs beginning with a :g:`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 reset
-
-      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 types. 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/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index a6dc15da55..5d257c7370 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,4 +1,4 @@
-.. _implicitcoercions:
+.. _coercions:
 
 Implicit Coercions
 ====================
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 2958d866ac..12fd038fb6 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -365,6 +365,21 @@ it is an atomic universe (i.e. not an algebraic max() universe).
 Explicit Universes
 -------------------
 
+.. insertprodn universe_name univ_constraint
+
+.. prodn::
+   universe_name ::= @qualid
+   | Set
+   | Prop
+   univ_annot ::= @%{ {* @universe_level } %}
+   universe_level ::= Set
+   | Prop
+   | Type
+   | _
+   | @qualid
+   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   univ_constraint ::= @universe_name {| < | = | <= } @universe_name
+
 The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
@@ -403,6 +418,37 @@ to universes and explicitly instantiate polymorphic definitions.
    .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead
       :undocumented:
 
+.. _printing-universes:
+
+Printing universes
+------------------
+
+.. flag:: Printing Universes
+
+   Turn this flag on to activate the display of the actual level of each
+   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in
+   combination with :flag:`Printing All` can help to diagnose failures to unify
+   terms apparently identical but internally different in the Calculus of Inductive
+   Constructions.
+
+.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string }
+   :name: Print Universes
+
+   This command can be used to print the constraints on the internal level
+   of the occurrences of :math:`\Type` (see :ref:`Sorts`).
+
+   The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting
+   constraints to preserve the implied transitive constraints between
+   kept universes).
+
+   The :n:`Sorted` clause makes each universe
+   equivalent to a numbered label reflecting its level (with a linear
+   ordering) in the universe hierarchy.
+
+   :n:`@string` is an optional output filename.
+   If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
+   language, and can be processed by Graphviz tools. The format is
+   unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
 Polymorphic definitions
 ~~~~~~~~~~~~~~~~~~~~~~~