diff options
| author | Clément Pit-Claudel | 2020-12-11 11:41:10 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-12-11 11:41:10 -0500 |
| commit | b6682484477d5ecb506c057cc2a9fe4ed883e22c (patch) | |
| tree | 6deadf84ebbe4c020c8a37e6de32f3ebcd368683 /doc/sphinx | |
| parent | c8d2248cbbe2c713605e0c61d7342fad948072da (diff) | |
doc: Clarify the status of simpl vs cbn
The cbn tactic was documented in aa9db490a2. The current manual causes
confusion by suggesting that cbn is a replacement for simpl, while in practice
they do different things, both with their own quirks. Given that neither is
consistently faster than the other, I think it's worth clarifying the manual.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index b7f2927000..3649202b45 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -522,7 +522,7 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + The :tacn:`cbn` tactic was intended to be a more principled, faster and more predictable replacement for :tacn:`simpl`. The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and |