changelog for more Ltac2 syntactic values

SkySkimmer · Jan 8, 2024 · 996d4df · 996d4df
1 parent 2f53ddd
commit 996d4df
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18411-ltac2-more-values.rst b/doc/changelog/06-Ltac2-language/18411-ltac2-more-values.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  recursive `let` and non mutable projections of syntactic values are considered syntactic values
+  (`#18411 <https://github.com/coq/coq/pull/18411>`_,
+  by Gaëtan Gilbert).