From b6682484477d5ecb506c057cc2a9fe4ed883e22c Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 11 Dec 2020 11:41:10 -0500
Subject: 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.
---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3