8 files changed, 63 insertions, 34 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1a1d31bdd7..468161ff73 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -676,6 +676,9 @@ library:ci-color:
 library:ci-compcert:
   extends: .ci-template-flambda
 
+library:ci-coq-tools:
+  extends: .ci-template
+
 library:ci-coqprime:
   stage: stage-3
   extends: .ci-template-flambda
diff --git a/Makefile.ci b/Makefile.ci
index 1a5e8166a2..b545c9de45 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -20,6 +20,7 @@ CI_TARGETS= \
     ci-coquelicot \
     ci-corn \
     ci-cross-crypto \
+    ci-coq-tools \
     ci-coqprime \
     ci-elpi \
     ci-ext-lib \
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6a740b9033..88d08a1724 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 ### Experimental automatic overlay creation and building
 
 If you break external projects that are hosted on GitHub, you can use
-the `create-overlays.sh` script to automatically perform most of the
+the `create_overlays.sh` script to automatically perform most of the
 above steps. In order to do so, call the script as:
 ```
-./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac
+./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
 ```
 replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
 number. The script will:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index c18e556da8..88f410ef04 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,6 +95,13 @@
 : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
+# coq-tools
+########################################################################
+: "${coq_tools_CI_REF:=master}"
+: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}"
+: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}"
+
+########################################################################
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq-tools.sh
new file mode 100755
index 0000000000..9c95c49c9f
--- /dev/null
+++ b/dev/ci/ci-coq-tools.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coq_tools
+
+( cd "${CI_BUILD_DIR}/coq_tools" && make check || \
+  { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } )
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index b2d3687780..b19239ed22 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -7,27 +7,26 @@ SProp (proof irrelevant propositions)
 
    The status of strict propositions is experimental.
 
+   In particular, conversion checking through bytecode or native code
+   compilation currently does not understand proof irrelevance.
+
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
 known as strict propositions) as described in
 :cite:`Gilbert:POPL2019`.
 
-Using :math:`\SProp` may be prevented by passing ``-disallow-sprop``
-to the |Coq| program or using :flag:`Allow StrictProp`.
+Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the
+|Coq| program or by turning the :flag:`Allow StrictProp` flag off.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
 
-   Allows using :math:`\SProp` when set and forbids it when unset. The
-   initial value depends on whether you used the command line
-   ``-disallow-sprop`` and ``-allow-sprop``.
-
-.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
-   :undocumented:
-
-.. coqtop:: none
+   Enables or disables the use of |SProp|.  It is enabled by default.
+   The command-line flag ``-disallow-sprop`` disables |SProp| at
+   startup.
 
-   Set Allow StrictProp.
+   .. exn:: SProp is disallowed because the "Allow StrictProp" flag is off.
+      :undocumented:
 
 Some of the definitions described in this document are available
 through ``Coq.Logic.StrictProp``, which see.
@@ -38,29 +37,35 @@ Basic constructs
 The purpose of :math:`\SProp` is to provide types where all elements
 are convertible:
 
-.. coqdoc::
+.. coqtop:: all
 
-   Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.
+   Theorem irrelevance (A : SProp) (P : A -> Prop) : forall x : A, P x -> forall y : A, P y.
+   Proof.
+   intros * Hx *.
+   exact Hx.
+   Qed.
 
 Since we have definitional :ref:`eta-expansion` for
 functions, the property of being a type of definitionally irrelevant
 values is impredicative, and so is :math:`\SProp`:
 
-.. coqdoc::
+.. coqtop:: all
 
    Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp.
 
-.. warning::
-
-   Conversion checking through bytecode or native code compilation
-   currently does not understand proof irrelevance.
-
 In order to keep conversion tractable, cumulativity for :math:`\SProp`
-is forbidden:
+is forbidden, unless the :flag:`Cumulative StrictProp` flag is turned
+on:
 
 .. coqtop:: all
 
    Fail Check (fun (A:SProp) => A : Type).
+   Set Cumulative StrictProp.
+   Check (fun (A:SProp) => A : Type).
+
+.. coqtop:: none
+
+   Unset Cumulative StrictProp.
 
 We can explicitly lift strict propositions into the relevant world by
 using a wrapping inductive type. The inductive stops definitional
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index fddc84b398..41f2ab9c63 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -729,9 +729,9 @@ let explain_undeclared_universe env sigma l =
     spc () ++ str "(maybe a bugged tactic)."
 
 let explain_disallowed_sprop () =
-  Pp.(strbrk "SProp not allowed, you need to "
-      ++ str "Set Allow StrictProp"
-      ++ strbrk " or to use the -allow-sprop command-line-flag.")
+  Pp.(strbrk "SProp is disallowed because the "
+      ++ str "\"Allow StrictProp\""
+      ++ strbrk " flag is off.")
 
 let explain_bad_relevance env =
   strbrk "Bad relevance (maybe a bugged tactic)."
diff --git a/vernac/library.ml b/vernac/library.ml
index afadbd704d..85db501e84 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -57,14 +57,18 @@ let in_delayed f ch ~segment =
 
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
-  try
-    let ch = open_in_bin f in
-    let () = LargeFile.seek_in ch pos in
-    let obj = System.marshal_in f ch in
-    let digest' = Digest.input ch in
-    if not (String.equal digest digest') then raise (Faulty f);
-    obj
-  with e when CErrors.noncritical e -> raise (Faulty f)
+  let ch = open_in_bin f in
+  let obj, digest' =
+    try
+      let () = LargeFile.seek_in ch pos in
+      let obj = System.marshal_in f ch in
+      let digest' = Digest.input ch in
+      obj, digest'
+    with e -> close_in ch; raise e
+  in
+  close_in ch;
+  if not (String.equal digest digest') then raise (Faulty f);
+  obj
 
 end
 
@@ -200,7 +204,7 @@ let access_table what tables dp i =
         with Faulty f ->
           user_err ~hdr:"Library.access_table"
             (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
-             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str ") is corrupted,\ncannot load some " ++
              str what ++ str " in it.\n")
       in
       tables := DPmap.add dp (Fetched t) !tables;