CHANGELOG for #6930.

agda · Oct 25, 2023 · 3ff92d3 · 3ff92d3
1 parent 6a4dd31
commit 3ff92d3
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -26,7 +26,10 @@ Additions to the Agda syntax.
 Language
 --------
 
-Changes of the type checker etc. that affect the Agda language.
+* A [change](https://github.com/agda/agda/pull/6639) in 2.6.4 that prevented all recursion on proofs,
+  i.e., members of a type `A : Prop ℓ`, has been [reverted](https://github.com/agda/agda/pull/6936).
+  It is possible again to use proofs as termination arguments.
+  (See [issue #6930](https://github.com/agda/agda/issues/6930).)
 
 Reflection
 ----------