diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 9b906d4317..13d983226b 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -51,8 +51,19 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
-/-- `cbv` performs simplification that closely mimics call-by-value evaluation,
-using equations associated with definitions and the matchers. -/
+/--
+`cbv` performs simplification that closely mimics call-by-value evaluation.
+It reduces the target term by unfolding definitions using their defining equations and
+applying matcher equations. The unfolding is propositional, so `cbv` also works
+with functions defined via well-founded recursion or partial fixpoints.
+
+The proofs produced by `cbv` only use the three standard axioms.
+In particular, they do not require trust in the correctness of the code
+generator.
+
+This tactic is experimental and its behavior is likely to change in upcoming
+releases of Lean.
+-/
 syntax (name := cbv) "cbv" : conv
 
 /--
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index d942e7e313..16f301c5bc 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -2299,7 +2299,8 @@ macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
 /--
 `cbv` performs simplification that closely mimics call-by-value evaluation.
 It reduces terms by unfolding definitions using their defining equations and
-applying matcher equations.
+applying matcher equations. The unfolding is propositional, so `cbv` also works
+with functions defined via well-founded recursion or partial fixpoints.
 
 `cbv` has built-in support for goals of the form `lhs = rhs`. It proceeds in
 two passes:
@@ -2313,6 +2314,10 @@ two passes:
 (simpler) equality goal. For goals that are not equalities, `cbv` currently
 leaves the goal unchanged.
 
+The proofs produced by `cbv` only use the three standard axioms.
+In particular, they do not require trust in the correctness of the code
+generator.
+
 This tactic is experimental and its behavior is likely to change in upcoming
 releases of Lean.
 -/
@@ -2329,6 +2334,10 @@ is a `Decidable` proposition. It proceeds in two steps:
 Unlike `cbv`, `decide_cbv` is a terminal tactic: it either closes the goal or
 fails.
 
+The proofs produced by `decide_cbv` only use the three standard axioms.
+In particular, they do not require trust in the correctness of the code
+generator.
+
 This tactic is experimental and its behavior is likely to change in upcoming
 releases of Lean.
 -/