From b6a925806f5eccf7510fe53416c52192c2ffb0a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Sep 2020 12:58:31 +0200
Subject: Make `simple apply in ...` point to `simple apply`

Instead, the example was duplicated.
---
 doc/sphinx/proof-engine/tactics.rst | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 5dc15a02c4..e276a0edcb 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -732,6 +732,7 @@ Applying theorems
       does not succeed because it would require the conversion of ``id ?foo`` and
       :g:`O`.
 
+      .. _simple_apply_ex:
       .. example::
 
          .. coqtop:: all
@@ -907,13 +908,8 @@ Applying theorems
    .. tacv:: simple apply @term in @ident
 
       This behaves like :tacn:`apply … in` but it reasons modulo conversion
-      only on subterms that contain no variables to instantiate. For instance,
-      if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and
-      :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it
-      would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is
-      an existential variable to instantiate.
-      Tactic :n:`simple apply @term in @ident` does not
-      either traverse tuples as :n:`apply @term in @ident` does.
+      only on subterms that contain no variables to instantiate and does not
+      traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`.
 
    .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern}
              {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern}
-- 
cgit v1.2.3