diff options
| author | Paolo G. Giarrusso | 2020-06-17 17:45:59 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-06-17 17:45:59 +0200 |
| commit | 5fbbf2f3f86909c68b97f4587de9fea07cdc0711 (patch) | |
| tree | b11a8a26af12e8bc334bf3e6fab685e602978ddb /doc/sphinx | |
| parent | 6499de1a834fa4e039246ac8b821ca23dd2a497e (diff) | |
tactics.rst: readd `cbv`
Hope this is enough, also looking at
https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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 |