From 5fbbf2f3f86909c68b97f4587de9fea07cdc0711 Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Wed, 17 Jun 2020 17:45:59 +0200
Subject: tactics.rst: readd `cbv`

Hope this is enough, also looking at
https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6290620ee1..4af3ebc47b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3045,7 +3045,7 @@ following:
 For backward compatibility, the notation :n:`in {+ @ident}` performs
 the conversion in hypotheses :n:`{+ @ident}`.
 
-.. tacn:: {? @strategy_flag }
+.. tacn:: cbv {? @strategy_flag }
           lazy {? @strategy_flag }
    :name: cbv; lazy
 
-- 
cgit v1.2.3