From 286a51836e4a6b0f710b125e6cc6b2b19e455ff3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Sep 2020 08:25:22 +0200
Subject: Improve `simple apply` example

The example showing the difference between `apply` and `simple apply`
used to depend on the order and the heuristics used on unification
problems. We make it independent for better clarity and stability.

Fixes https://github.com/coq/coq/issues/13023
---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2f505e7448..5dc15a02c4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -737,7 +737,7 @@ Applying theorems
          .. coqtop:: all
 
             Definition id (x : nat) := x.
-            Parameter H : forall y, id y = y.
+            Parameter H : forall x y, id x = y.
             Goal O = O.
             Fail simple apply H.
 
-- 
cgit v1.2.3