From 80ff25b75839f792add3a66d9896d69f0065c6d8 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 25 May 2018 18:35:30 -0400
Subject: [doc] Allow more than one signature and name per Sphinx object

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

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2b128b98fe..88c1e225fd 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -178,7 +178,7 @@ Sequence
 A sequence is an expression of the following form:
 
 .. tacn:: @expr ; @expr
-   :name: ;
+   :name: ltac-seq
 
    The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be
    a tactic value. The tactic :n:`v__1` is applied to the current goal,
-- 
cgit v1.2.3