Merge PR #13619: doc: Clarify the status of simpl vs cbn

Reviewed-by: Zimmi48
coq · Dec 13, 2020 · a819eee · a819eee
2 parents 81d0936 + b668248
commit a819eee
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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