diff options
| author | coqbot-app[bot] | 2020-12-13 19:04:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-13 19:04:06 +0000 |
| commit | a819eeed1770f393577e6df42220cba25787887d (patch) | |
| tree | 4ceccb35ead0a1b2ed55611d8aba2ada4425f9f9 /doc | |
| parent | 81d0936c1ac8a537b5d8083933bce607e55ff28f (diff) | |
| parent | b6682484477d5ecb506c057cc2a9fe4ed883e22c (diff) | |
Merge PR #13619: doc: Clarify the status of simpl vs cbn
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
| -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 |