aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/changelog/01-kernel/10811-sprop-default-on.rst3
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst
new file mode 100644
index 0000000000..349c44c205
--- /dev/null
+++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst
@@ -0,0 +1,3 @@
+- Using ``SProp`` is now allowed by default, without needing to pass
+ ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811
+ <https://github.com/coq/coq/pull/10811>`_, by Gaƫtan Gilbert).