[refman] Move all the Ltac examples to the Ltac chapter.

The Detailed examples of tactics chapter can be removed when the
remaining examples are moved closer to the definitions of the
corresponding tactics.

This commit also moves back the footnotes from the Tactics chapter at
the end of the chapter, and removes an old footnote that doesn't
matter anymore.

3 files changed, 414 insertions, 424 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index b629d15b11..0ace9ef5b9 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command.
    .. coqtop:: none
 
       Qed.
-
-Using the tactic language
--------------------------
-
-
-About the cardinality of the set of natural numbers
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The first example which shows how to use pattern matching over the
-proof context is a proof of the fact that natural numbers have more
-than two elements. This can be done as follows:
-
-.. coqtop:: in reset
-
-   Lemma card_nat :
-     ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
-   Proof.
-
-.. coqtop:: in
-
-   red; intros (x, (y, Hy)).
-
-.. coqtop:: in
-
-   elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
-
-   match goal with
-       | _ : ?a = ?b, _ : ?a = ?c |- _ =>
-           cut (b = c); [ discriminate | transitivity a; auto ]
-   end.
-
-.. coqtop:: in
-
-   Qed.
-
-We can notice that all the (very similar) cases coming from the three
-eliminations (with three distinct natural numbers) are successfully
-solved by a match goal structure and, in particular, with only one
-pattern (use of non-linear matching).
-
-
-Permutations of lists
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A more complex example is the problem of permutations of
-lists. The aim is to show that a list is a permutation of
-another list.
-
-.. coqtop:: in reset
-
-   Section Sort.
-
-.. coqtop:: in
-
-   Variable A : Set.
-
-.. coqtop:: in
-
-   Inductive perm : list A -> list A -> Prop :=
-       | perm_refl : forall l, perm l l
-       | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
-       | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
-       | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
-
-.. coqtop:: in
-
-   End Sort.
-
-First, we define the permutation predicate as shown above.
-
-.. coqtop:: none
-
-   Require Import List.
-
-
-.. coqtop:: in
-
-   Ltac perm_aux n :=
-   match goal with
-       | |- (perm _ ?l ?l) => apply perm_refl
-       | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
-           let newn := eval compute in (length l1) in
-               (apply perm_cons; perm_aux newn)
-       | |- (perm ?A (?a :: ?l1) ?l2) =>
-           match eval compute in n with
-               | 1 => fail
-               | _ =>
-                   let l1' := constr:(l1 ++ a :: nil) in
-                       (apply (perm_trans A (a :: l1) l1' l2);
-                       [ apply perm_append | compute; perm_aux (pred n) ])
-           end
-   end.
-
-Next we define an auxiliary tactic ``perm_aux`` which takes an argument
-used to control the recursion depth. This tactic behaves as follows. If
-the lists are identical (i.e. convertible), it concludes. Otherwise, if
-the lists have identical heads, it proceeds to look at their tails.
-Finally, if the lists have different heads, it rotates the first list by
-putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the
-number of performed rotations using the argument ``n``. We do this by
-decrementing ``n`` each time we perform a rotation. It works because
-for a list of length ``n`` we can make exactly ``n - 1`` rotations
-to generate at most ``n`` distinct lists. Notice that we use the natural
-numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know
-that it is possible to use the usual natural numbers, but they are only
-used as arguments for primitive tactics and they cannot be handled, so,
-in particular, we cannot make computations with them. Thus the natural
-choice is to use Coq data structures so that Coq makes the computations
-(reductions) by ``eval compute in`` and we can get the terms back by match.
-
-.. coqtop:: in
-
-   Ltac solve_perm :=
-   match goal with
-       | |- (perm _ ?l1 ?l2) =>
-           match eval compute in (length l1 = length l2) with
-               | (?n = ?n) => perm_aux n
-           end
-   end.
-
-The main tactic is ``solve_perm``. It computes the lengths of the two lists
-and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they
-aren't, the lists cannot be permutations of each other). Using this tactic we
-can now prove lemmas as follows:
-
-.. coqtop:: in
-
-   Lemma solve_perm_ex1 :
-     perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
-   Proof. solve_perm. Qed.
-
-.. coqtop:: in
-
-   Lemma solve_perm_ex2 :
-     perm nat
-       (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
-         (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
-   Proof. solve_perm. Qed.
-
-Deciding intuitionistic propositional logic
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Pattern matching on goals allows a powerful backtracking when returning tactic
-values. An interesting application is the problem of deciding intuitionistic
-propositional logic. Considering the contraction-free sequent calculi LJT* of
-Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
-tactic language as shown below.
-
-.. coqtop:: in reset
-
-   Ltac basic :=
-   match goal with
-       | |- True => trivial
-       | _ : False |- _ => contradiction
-       | _ : ?A |- ?A => assumption
-   end.
-
-.. coqtop:: in
-
-   Ltac simplify :=
-   repeat (intros;
-       match goal with
-           | H : ~ _ |- _ => red in H
-           | H : _ /\ _ |- _ =>
-               elim H; do 2 intro; clear H
-           | H : _ \/ _ |- _ =>
-               elim H; intro; clear H
-           | H : ?A /\ ?B -> ?C |- _ =>
-               cut (A -> B -> C);
-                   [ intro | intros; apply H; split; assumption ]
-           | H: ?A \/ ?B -> ?C |- _ =>
-               cut (B -> C);
-                   [ cut (A -> C);
-                       [ intros; clear H
-                       | intro; apply H; left; assumption ]
-                   | intro; apply H; right; assumption ]
-           | H0 : ?A -> ?B, H1 : ?A |- _ =>
-               cut B; [ intro; clear H0 | apply H0; assumption ]
-           | |- _ /\ _ => split
-           | |- ~ _ => red
-       end).
-
-.. coqtop:: in
-
-   Ltac my_tauto :=
-     simplify; basic ||
-     match goal with
-         | H : (?A -> ?B) -> ?C |- _ =>
-             cut (B -> C);
-                 [ intro; cut (A -> B);
-                     [ intro; cut C;
-                         [ intro; clear H | apply H; assumption ]
-                     | clear H ]
-                 | intro; apply H; intro; assumption ]; my_tauto
-         | H : ~ ?A -> ?B |- _ =>
-             cut (False -> B);
-                 [ intro; cut (A -> False);
-                     [ intro; cut B;
-                         [ intro; clear H | apply H; assumption ]
-                     | clear H ]
-                 | intro; apply H; red; intro; assumption ]; my_tauto
-         | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
-     end.
-
-The tactic ``basic`` tries to reason using simple rules involving truth, falsity
-and available assumptions. The tactic ``simplify`` applies all the reversible
-rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
-tactic to be called) simplifies with ``simplify``, tries to conclude with
-``basic`` and tries several paths using the backtracking rules (one of the
-four Dyckhoff’s rules for the left implication to get rid of the contraction
-and the right ``or``).
-
-Having defined ``my_tauto``, we can prove tautologies like these:
-
-.. coqtop:: in
-
-   Lemma my_tauto_ex1 :
-     forall A B : Prop, A /\ B -> A \/ B.
-   Proof. my_tauto. Qed.
-
-.. coqtop:: in
-
-   Lemma my_tauto_ex2 :
-     forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
-   Proof. my_tauto. Qed.
-
-
-Deciding type isomorphisms
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A more tricky problem is to decide equalities between types modulo
-isomorphisms. Here, we choose to use the isomorphisms of the simply
-typed λ-calculus with Cartesian product and unit type (see, for
-example, :cite:`RC95`). The axioms of this λ-calculus are given below.
-
-.. coqtop:: in reset
-
-   Open Scope type_scope.
-
-.. coqtop:: in
-
-   Section Iso_axioms.
-
-.. coqtop:: in
-
-   Variables A B C : Set.
-
-.. coqtop:: in
-
-   Axiom Com : A * B = B * A.
-
-   Axiom Ass : A * (B * C) = A * B * C.
-
-   Axiom Cur : (A * B -> C) = (A -> B -> C).
-
-   Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
-
-   Axiom P_unit : A * unit = A.
-
-   Axiom AR_unit : (A -> unit) = unit.
-
-   Axiom AL_unit : (unit -> A) = A.
-
-.. coqtop:: in
-
-   Lemma Cons : B = C -> A * B = A * C.
-
-   Proof.
-
-   intro Heq; rewrite Heq; reflexivity.
-
-   Qed.
-
-.. coqtop:: in
-
-   End Iso_axioms.
-
-.. coqtop:: in
-
-   Ltac simplify_type ty :=
-   match ty with
-       | ?A * ?B * ?C =>
-           rewrite <- (Ass A B C); try simplify_type_eq
-       | ?A * ?B -> ?C =>
-           rewrite (Cur A B C); try simplify_type_eq
-       | ?A -> ?B * ?C =>
-           rewrite (Dis A B C); try simplify_type_eq
-       | ?A * unit =>
-           rewrite (P_unit A); try simplify_type_eq
-       | unit * ?B =>
-           rewrite (Com unit B); try simplify_type_eq
-       | ?A -> unit =>
-           rewrite (AR_unit A); try simplify_type_eq
-       | unit -> ?B =>
-           rewrite (AL_unit B); try simplify_type_eq
-       | ?A * ?B =>
-           (simplify_type A; try simplify_type_eq) ||
-           (simplify_type B; try simplify_type_eq)
-       | ?A -> ?B =>
-           (simplify_type A; try simplify_type_eq) ||
-           (simplify_type B; try simplify_type_eq)
-   end
-   with simplify_type_eq :=
-   match goal with
-       | |- ?A = ?B => try simplify_type A; try simplify_type B
-   end.
-
-.. coqtop:: in
-
-   Ltac len trm :=
-   match trm with
-       | _ * ?B => let succ := len B in constr:(S succ)
-       | _ => constr:(1)
-   end.
-
-.. coqtop:: in
-
-   Ltac assoc := repeat rewrite <- Ass.
-
-.. coqtop:: in
-
-   Ltac solve_type_eq n :=
-   match goal with
-       | |- ?A = ?A => reflexivity
-       | |- ?A * ?B = ?A * ?C =>
-           apply Cons; let newn := len B in solve_type_eq newn
-       | |- ?A * ?B = ?C =>
-           match eval compute in n with
-               | 1 => fail
-               | _ =>
-                   pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n)
-           end
-   end.
-
-.. coqtop:: in
-
-   Ltac compare_structure :=
-   match goal with
-       | |- ?A = ?B =>
-           let l1 := len A
-           with l2 := len B in
-               match eval compute in (l1 = l2) with
-                   | ?n = ?n => solve_type_eq n
-               end
-   end.
-
-.. coqtop:: in
-
-   Ltac solve_iso := simplify_type_eq; compare_structure.
-
-The tactic to judge equalities modulo this axiomatization is shown above.
-The algorithm is quite simple. First types are simplified using axioms that
-can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
-The normal forms are sequences of Cartesian products without Cartesian product
-in the left component. These normal forms are then compared modulo permutation
-of the components by the tactic ``compare_structure``. If they have the same
-lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
-The main tactic that puts all these components together is called ``solve_iso``.
-
-Here are examples of what can be solved by ``solve_iso``.
-
-.. coqtop:: in
-
-   Lemma solve_iso_ex1 :
-     forall A B : Set, A * unit * B = B * (unit * A).
-   Proof.
-     intros; solve_iso.
-   Qed.
-
-.. coqtop:: in
-
-   Lemma solve_iso_ex2 :
-     forall A B C : Set,
-       (A * unit -> B * (C * unit)) =
-       (A * unit -> (C -> unit) * C) * (unit -> A -> B).
-   Proof.
-     intros; solve_iso.
-   Qed.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index d3562b52c5..d35e4ab782 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -3,12 +3,25 @@
 Ltac
 ====
 
-This chapter gives a compact documentation of |Ltac|, the tactic language
-available in |Coq|. We start by giving the syntax, and next, we present the
-informal semantics. If you want to know more regarding this language and
-especially about its foundations, you can refer to :cite:`Del00`. Chapter
-:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial
-use examples of this language.
+This chapter documents the tactic language |Ltac|.
+
+We start by giving the syntax, and next, we present the informal
+semantics. If you want to know more regarding this language and
+especially about its foundations, you can refer to :cite:`Del00`.
+
+.. example::
+
+   Here are some examples of the kind of tactic macros that this
+   language allows to write.
+
+   .. coqdoc::
+
+      Ltac reduce_and_try_to_solve := simpl; intros; auto.
+
+      Ltac destruct_bool_and_rewrite b H1 H2 :=
+        destruct b; [ rewrite H1; eauto | rewrite H2; eauto ].
+
+   Some more advanced examples are given in Section :ref:`ltac-examples`.
 
 .. _ltac-syntax:
 
@@ -1160,6 +1173,388 @@ Printing |Ltac| tactics
 
    This command displays a list of all user-defined tactics, with their arguments.
 
+
+.. _ltac-examples:
+
+Examples of using |Ltac|
+-------------------------
+
+
+About the cardinality of the set of natural numbers
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The first example which shows how to use pattern matching over the
+proof context is a proof of the fact that natural numbers have more
+than two elements. This can be done as follows:
+
+.. coqtop:: in reset
+
+   Lemma card_nat :
+     ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
+   Proof.
+
+.. coqtop:: in
+
+   red; intros (x, (y, Hy)).
+
+.. coqtop:: in
+
+   elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
+
+   match goal with
+       | _ : ?a = ?b, _ : ?a = ?c |- _ =>
+           cut (b = c); [ discriminate | transitivity a; auto ]
+   end.
+
+.. coqtop:: in
+
+   Qed.
+
+We can notice that all the (very similar) cases coming from the three
+eliminations (with three distinct natural numbers) are successfully
+solved by a match goal structure and, in particular, with only one
+pattern (use of non-linear matching).
+
+
+Permutations of lists
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A more complex example is the problem of permutations of
+lists. The aim is to show that a list is a permutation of
+another list.
+
+.. coqtop:: in reset
+
+   Section Sort.
+
+.. coqtop:: in
+
+   Variable A : Set.
+
+.. coqtop:: in
+
+   Inductive perm : list A -> list A -> Prop :=
+       | perm_refl : forall l, perm l l
+       | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
+       | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
+       | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
+
+.. coqtop:: in
+
+   End Sort.
+
+First, we define the permutation predicate as shown above.
+
+.. coqtop:: none
+
+   Require Import List.
+
+
+.. coqtop:: in
+
+   Ltac perm_aux n :=
+   match goal with
+       | |- (perm _ ?l ?l) => apply perm_refl
+       | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
+           let newn := eval compute in (length l1) in
+               (apply perm_cons; perm_aux newn)
+       | |- (perm ?A (?a :: ?l1) ?l2) =>
+           match eval compute in n with
+               | 1 => fail
+               | _ =>
+                   let l1' := constr:(l1 ++ a :: nil) in
+                       (apply (perm_trans A (a :: l1) l1' l2);
+                       [ apply perm_append | compute; perm_aux (pred n) ])
+           end
+   end.
+
+Next we define an auxiliary tactic ``perm_aux`` which takes an argument
+used to control the recursion depth. This tactic behaves as follows. If
+the lists are identical (i.e. convertible), it concludes. Otherwise, if
+the lists have identical heads, it proceeds to look at their tails.
+Finally, if the lists have different heads, it rotates the first list by
+putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the
+number of performed rotations using the argument ``n``. We do this by
+decrementing ``n`` each time we perform a rotation. It works because
+for a list of length ``n`` we can make exactly ``n - 1`` rotations
+to generate at most ``n`` distinct lists. Notice that we use the natural
+numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know
+that it is possible to use the usual natural numbers, but they are only
+used as arguments for primitive tactics and they cannot be handled, so,
+in particular, we cannot make computations with them. Thus the natural
+choice is to use Coq data structures so that Coq makes the computations
+(reductions) by ``eval compute in`` and we can get the terms back by match.
+
+.. coqtop:: in
+
+   Ltac solve_perm :=
+   match goal with
+       | |- (perm _ ?l1 ?l2) =>
+           match eval compute in (length l1 = length l2) with
+               | (?n = ?n) => perm_aux n
+           end
+   end.
+
+The main tactic is ``solve_perm``. It computes the lengths of the two lists
+and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they
+aren't, the lists cannot be permutations of each other). Using this tactic we
+can now prove lemmas as follows:
+
+.. coqtop:: in
+
+   Lemma solve_perm_ex1 :
+     perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+   Proof. solve_perm. Qed.
+
+.. coqtop:: in
+
+   Lemma solve_perm_ex2 :
+     perm nat
+       (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+         (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+   Proof. solve_perm. Qed.
+
+Deciding intuitionistic propositional logic
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Pattern matching on goals allows a powerful backtracking when returning tactic
+values. An interesting application is the problem of deciding intuitionistic
+propositional logic. Considering the contraction-free sequent calculi LJT* of
+Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
+tactic language as shown below.
+
+.. coqtop:: in reset
+
+   Ltac basic :=
+   match goal with
+       | |- True => trivial
+       | _ : False |- _ => contradiction
+       | _ : ?A |- ?A => assumption
+   end.
+
+.. coqtop:: in
+
+   Ltac simplify :=
+   repeat (intros;
+       match goal with
+           | H : ~ _ |- _ => red in H
+           | H : _ /\ _ |- _ =>
+               elim H; do 2 intro; clear H
+           | H : _ \/ _ |- _ =>
+               elim H; intro; clear H
+           | H : ?A /\ ?B -> ?C |- _ =>
+               cut (A -> B -> C);
+                   [ intro | intros; apply H; split; assumption ]
+           | H: ?A \/ ?B -> ?C |- _ =>
+               cut (B -> C);
+                   [ cut (A -> C);
+                       [ intros; clear H
+                       | intro; apply H; left; assumption ]
+                   | intro; apply H; right; assumption ]
+           | H0 : ?A -> ?B, H1 : ?A |- _ =>
+               cut B; [ intro; clear H0 | apply H0; assumption ]
+           | |- _ /\ _ => split
+           | |- ~ _ => red
+       end).
+
+.. coqtop:: in
+
+   Ltac my_tauto :=
+     simplify; basic ||
+     match goal with
+         | H : (?A -> ?B) -> ?C |- _ =>
+             cut (B -> C);
+                 [ intro; cut (A -> B);
+                     [ intro; cut C;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; intro; assumption ]; my_tauto
+         | H : ~ ?A -> ?B |- _ =>
+             cut (False -> B);
+                 [ intro; cut (A -> False);
+                     [ intro; cut B;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; red; intro; assumption ]; my_tauto
+         | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
+     end.
+
+The tactic ``basic`` tries to reason using simple rules involving truth, falsity
+and available assumptions. The tactic ``simplify`` applies all the reversible
+rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
+tactic to be called) simplifies with ``simplify``, tries to conclude with
+``basic`` and tries several paths using the backtracking rules (one of the
+four Dyckhoff’s rules for the left implication to get rid of the contraction
+and the right ``or``).
+
+Having defined ``my_tauto``, we can prove tautologies like these:
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex1 :
+     forall A B : Prop, A /\ B -> A \/ B.
+   Proof. my_tauto. Qed.
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex2 :
+     forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+   Proof. my_tauto. Qed.
+
+
+Deciding type isomorphisms
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A more tricky problem is to decide equalities between types modulo
+isomorphisms. Here, we choose to use the isomorphisms of the simply
+typed λ-calculus with Cartesian product and unit type (see, for
+example, :cite:`RC95`). The axioms of this λ-calculus are given below.
+
+.. coqtop:: in reset
+
+   Open Scope type_scope.
+
+.. coqtop:: in
+
+   Section Iso_axioms.
+
+.. coqtop:: in
+
+   Variables A B C : Set.
+
+.. coqtop:: in
+
+   Axiom Com : A * B = B * A.
+
+   Axiom Ass : A * (B * C) = A * B * C.
+
+   Axiom Cur : (A * B -> C) = (A -> B -> C).
+
+   Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+
+   Axiom P_unit : A * unit = A.
+
+   Axiom AR_unit : (A -> unit) = unit.
+
+   Axiom AL_unit : (unit -> A) = A.
+
+.. coqtop:: in
+
+   Lemma Cons : B = C -> A * B = A * C.
+
+   Proof.
+
+   intro Heq; rewrite Heq; reflexivity.
+
+   Qed.
+
+.. coqtop:: in
+
+   End Iso_axioms.
+
+.. coqtop:: in
+
+   Ltac simplify_type ty :=
+   match ty with
+       | ?A * ?B * ?C =>
+           rewrite <- (Ass A B C); try simplify_type_eq
+       | ?A * ?B -> ?C =>
+           rewrite (Cur A B C); try simplify_type_eq
+       | ?A -> ?B * ?C =>
+           rewrite (Dis A B C); try simplify_type_eq
+       | ?A * unit =>
+           rewrite (P_unit A); try simplify_type_eq
+       | unit * ?B =>
+           rewrite (Com unit B); try simplify_type_eq
+       | ?A -> unit =>
+           rewrite (AR_unit A); try simplify_type_eq
+       | unit -> ?B =>
+           rewrite (AL_unit B); try simplify_type_eq
+       | ?A * ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+       | ?A -> ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+   end
+   with simplify_type_eq :=
+   match goal with
+       | |- ?A = ?B => try simplify_type A; try simplify_type B
+   end.
+
+.. coqtop:: in
+
+   Ltac len trm :=
+   match trm with
+       | _ * ?B => let succ := len B in constr:(S succ)
+       | _ => constr:(1)
+   end.
+
+.. coqtop:: in
+
+   Ltac assoc := repeat rewrite <- Ass.
+
+.. coqtop:: in
+
+   Ltac solve_type_eq n :=
+   match goal with
+       | |- ?A = ?A => reflexivity
+       | |- ?A * ?B = ?A * ?C =>
+           apply Cons; let newn := len B in solve_type_eq newn
+       | |- ?A * ?B = ?C =>
+           match eval compute in n with
+               | 1 => fail
+               | _ =>
+                   pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n)
+           end
+   end.
+
+.. coqtop:: in
+
+   Ltac compare_structure :=
+   match goal with
+       | |- ?A = ?B =>
+           let l1 := len A
+           with l2 := len B in
+               match eval compute in (l1 = l2) with
+                   | ?n = ?n => solve_type_eq n
+               end
+   end.
+
+.. coqtop:: in
+
+   Ltac solve_iso := simplify_type_eq; compare_structure.
+
+The tactic to judge equalities modulo this axiomatization is shown above.
+The algorithm is quite simple. First types are simplified using axioms that
+can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
+The normal forms are sequences of Cartesian products without Cartesian product
+in the left component. These normal forms are then compared modulo permutation
+of the components by the tactic ``compare_structure``. If they have the same
+lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
+The main tactic that puts all these components together is called ``solve_iso``.
+
+Here are examples of what can be solved by ``solve_iso``.
+
+.. coqtop:: in
+
+   Lemma solve_iso_ex1 :
+     forall A B : Set, A * unit * B = B * (unit * A).
+   Proof.
+     intros; solve_iso.
+   Qed.
+
+.. coqtop:: in
+
+   Lemma solve_iso_ex2 :
+     forall A B C : Set,
+       (A * unit -> B * (C * unit)) =
+       (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+   Proof.
+     intros; solve_iso.
+   Qed.
+
+
 Debugging |Ltac| tactics
 ------------------------
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 0f78a9b84a..c728b925ac 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3561,7 +3561,7 @@ Automation
 .. tacn:: autorewrite with {+ @ident}
    :name: autorewrite
 
-   This tactic [4]_ carries out rewritings according to the rewriting rule
+   This tactic carries out rewritings according to the rewriting rule
    bases :n:`{+ @ident}`.
 
    Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
@@ -4661,9 +4661,12 @@ Non-logical tactics
 
 .. example::
 
-   .. coqtop:: all reset
+   .. coqtop:: none reset
 
       Parameter P : nat -> Prop.
+
+   .. coqtop:: all abort
+
       Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
       repeat split.
       all: cycle 2.
@@ -4679,9 +4682,8 @@ Non-logical tactics
 
 .. example::
 
-   .. coqtop:: reset all
+   .. coqtop:: all abort
 
-      Parameter P : nat -> Prop.
       Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
       repeat split.
       all: swap 1 3.
@@ -4694,9 +4696,8 @@ Non-logical tactics
 
    .. example::
 
-      .. coqtop:: all reset
+      .. coqtop:: all abort
 
-         Parameter P : nat -> Prop.
          Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
          repeat split.
          all: revgoals.
@@ -4717,7 +4718,7 @@ Non-logical tactics
 
       .. example::
 
-         .. coqtop:: all reset
+         .. coqtop:: all abort
 
             Goal exists n, n=0.
             refine (ex_intro _ _ _).
@@ -4746,39 +4747,6 @@ Non-logical tactics
    The ``give_up`` tactic can be used while editing a proof, to choose to
    write the proof script in a non-sequential order.
 
-Simple tactic macros
--------------------------
-
-A simple example has more value than a long explanation:
-
-.. example::
-
-   .. coqtop:: reset all
-
-      Ltac Solve := simpl; intros; auto.
-
-      Ltac ElimBoolRewrite b H1 H2 :=
-      elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].
-
-The tactics macros are synchronous with the Coq section mechanism: a
-tactic definition is deleted from the current environment when you
-close the section (see also :ref:`section-mechanism`) where it was
-defined. If you want that a tactic macro defined in a module is usable in the
-modules that require it, you should put it outside of any section.
-
-:ref:`ltac` gives examples of more complex
-user-defined tactics.
-
-.. [1] Actually, only the second subgoal will be generated since the
-  other one can be automatically checked.
-.. [2] This corresponds to the cut rule of sequent calculus.
-.. [3] Reminder: opaque constants will not be expanded by δ reductions.
-.. [4] The behavior of this tactic has changed a lot compared to the
-  versions available in the previous distributions (V6). This may cause
-  significant changes in your theories to obtain the same result. As a
-  drawback of the re-engineering of the code, this tactic has also been
-  completely revised to get a very compact and readable version.
-
 Delaying solving unification constraints
 ----------------------------------------
 
@@ -4917,3 +4885,8 @@ Performance-oriented tactic variants
             Goal False.
               native_cast_no_check I.
             Fail Qed.
+
+.. [1] Actually, only the second subgoal will be generated since the
+  other one can be automatically checked.
+.. [2] This corresponds to the cut rule of sequent calculus.
+.. [3] Reminder: opaque constants will not be expanded by δ reductions.