diff options
| author | Théo Zimmermann | 2020-06-18 09:18:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-18 09:18:46 +0200 |
| commit | 33e763a441022623621536766ac38c3021dcb65c (patch) | |
| tree | b11a8a26af12e8bc334bf3e6fab685e602978ddb /doc/sphinx/proof-engine | |
| parent | 6499de1a834fa4e039246ac8b821ca23dd2a497e (diff) | |
| parent | 5fbbf2f3f86909c68b97f4587de9fea07cdc0711 (diff) | |
Merge PR #12536: tactics.rst: fix typo — readd `cbv` to title of its section
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/proof-engine')
| -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 |