From e68bccba9344c1b3d77d3e815af6cce1ce50b731 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 21 Mar 2019 10:08:29 +0100
Subject: [ssr] new syntax for the under tactic

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

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a4ab038314..cb529bd68e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3692,9 +3692,7 @@ complete terms, as shown by the simple example below.
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G by rewrite subnn.
-
-  ``(* FIXME: replace with do... *)``
+      under eq_G => n do rewrite subnn.
 
 .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
    :name: under
@@ -3762,7 +3760,7 @@ lemma ``eq_G``, but this time in interactive mode:
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G.
+      under eq_G => m.
         rewrite subnn.
         over.
 
@@ -3857,9 +3855,7 @@ shortened to: :n:`under @term => i do tac1.`
       Lemma test_big_nested (F G : nat -> nat) (m n : nat) :
         \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
         \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
-      under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC].
-
-   ``(* FIXME: replace with do... *)``
+      under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC].
 
 .. _locking_ssr:
 
-- 
cgit v1.2.3