aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-10-14 07:05:01 +0200
committerPierre-Marie Pédrot2019-10-14 07:05:01 +0200
commit54e31c28bf21caf7f8fcff1fcf4b415fed66dc3a (patch)
tree038374a730db66e8a2284f7b186925a654a7369e /doc/changelog
parent7623da4448381955ef063dcce6f4263d91fe0d74 (diff)
parent825d0737069debb8e16c44cd49ad3a273211f76c (diff)
Merge PR #10811: Allow SProp default on
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
Diffstat (limited to 'doc/changelog')
-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).