diff --git a/CHANGELOG.md b/CHANGELOG.md
index aff5d2f3f046f1c2f0702d843251c4b71765c5e4..89c1880fa9870de952817a9a5d4f686539ac349c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 Changes in and extensions of the theory:
 
-* [#] Weakestpre for total program correctness.
+* [#] Add weakest preconditions for total program correctness.
+* [#] "(Potentially) stuck" weakest preconditions are no longer considered
+  experimental.
 
 Changes in Coq: