diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-reduction_effects.sh | 8 | ||||
| -rw-r--r-- | dev/doc/changes.md | 7 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
4 files changed, 25 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9e9e3b4cfa..7342bc72e7 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -259,6 +259,13 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## +# reduction-effects +######################################################################## +: "${reduction_effects_CI_REF:=master}" +: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}" +: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}" + +######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh new file mode 100755 index 0000000000..6b6de3fa2f --- /dev/null +++ b/dev/ci/ci-reduction_effects.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download reduction_effects + +( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..3bc92e6aee 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,13 @@ ### ML API +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 835c20a4f7..f640a33773 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -254,7 +254,9 @@ let ppenvwithcst e = pp let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) -let ppobj obj = Format.print_string (Libobject.object_tag obj) +let ppobj obj = + let Libobject.Dyn.Dyn (tag, _) = obj in + Format.print_string (Libobject.Dyn.repr tag) let cnt = ref 0 |