From b95021b2943ea4d5b64396fe8154516040dbbe88 Mon Sep 17 00:00:00 2001
From: hawnzug
Date: Fri, 8 Mar 2019 19:04:18 +0800
Subject: [sphinx] Fix typo in local application of tactics

---
 doc/sphinx/proof-engine/ltac.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 3e87e8acd8..52e3029b8f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -200,7 +200,7 @@ following form:
    :name: [> ... | ... | ... ] (dispatch)
 
    The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for
-   i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the
+   i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the
    i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not
    exactly n.
 
-- 
cgit v1.2.3