diff options
| -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 |