aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.md
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-03-15 14:19:51 +0100
committerPierre-Marie Pédrot2019-03-15 14:19:51 +0100
commited275fd5eb8b11003f8904010d853d2bd568db79 (patch)
treee27b7778175cb0d9d19bd8bde9c593b335a85125 /dev/doc/changes.md
parenta44c4a34202fa6834520fcd6842cc98eecf044ec (diff)
parent1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff)
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: mattam82
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r--dev/doc/changes.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 491a75bb3d..d515ec30e8 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,6 +12,8 @@
### ML API
+SProp was added, see <SProp.md>
+
General deprecation
- All functions marked [@@ocaml.deprecated] in 8.8 have been