aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/ci-basic-overlay.sh2
-rw-r--r--dev/doc/changes.md6
2 files changed, 7 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c37b3133e..59a71b6086 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -80,7 +80,7 @@
# VST
########################################################################
: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
########################################################################
# fiat_parsers
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 5be8257e87..707adce308 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -24,6 +24,12 @@ passing `-bypass-API`.
### ML API
+General deprecation
+
+- All functions marked [@@ocaml.deprecated] in 8.7 have been
+ removed. Please, make sure your plugin is warning-free in 8.7 before
+ trying to port it over 8.8.
+
We removed the following functions:
- `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`