From adfcba52e84d071b0c82dae8424d01be7f4a06cb Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita
Date: Wed, 29 Jul 2020 17:39:26 +0900
Subject: Fix do in ssreflect-proof-language.rst

The tactics do in SSReflect uses `? @mult` rather than `? @num`.---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7b3670164b..3b4b80ca21 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2280,7 +2280,7 @@ to the others.
 Iteration
 ~~~~~~~~~
 
-.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
+.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] }
    :name: do (ssreflect)
 
    This tactical offers an accurate control on the repetition of tactics.
-- 
cgit v1.2.3