From bcf64b062a1dde1e2322e84cb041607bf76b0b78 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Oct 2018 11:42:01 +0000
Subject: [Manual] Avoid using deprecated “Focus”

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index bcef988874..6fde52f95e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2486,8 +2486,7 @@ destruction of existential assumptions like in the tactic:
   .. coqtop:: all
 
      Lemma test : True.
-     have [x Px]: exists x : nat, x > 0.
-     Focus 2.
+     have [x Px]: exists x : nat, x > 0; last first.
 
 An alternative use of the ``have`` tactic is to provide the explicit proof
 term for the intermediate lemma, using tactics of the form:
@@ -2565,8 +2564,7 @@ copying the goal itself.
   .. coqtop:: all
 
      Lemma test : True.
-     have suff H : 2 + 2 = 3.
-     Focus 2.
+     have suff H : 2 + 2 = 3; last first.
 
   Note that H is introduced in the second goal.
 
@@ -2853,8 +2851,7 @@ pattern will be used to process its instance.
   .. coqtop:: all
 
      Lemma simple n (ngt0 : 0 < n ) : P n.
-     gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0).
-     Focus 2.
+     gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first.
 
 
 .. _advanced_generalization_ssr:
-- 
cgit v1.2.3