From c59815c860a11948359e96ecc51d566bb5e5d8fb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 25 Oct 2019 15:28:37 -0400
Subject: `assert_succeeds`&`assert_fails`: multisuccess fix

These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.

Fixes #10965
---
 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 79eddbd3b5..aa4e90560b 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -516,7 +516,7 @@ Coq provides a derived tactic to check that a tactic *fails*:
 .. tacn:: assert_fails @ltac_expr
    :name: assert_fails
 
-   This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`.
+   This behaves like :n:`tryif once @ltac_expr then fail 0 tac "succeeds" else idtac`.
 
 Checking the success
 ~~~~~~~~~~~~~~~~~~~~
-- 
cgit v1.2.3