diff --git a/README.md b/README.md
index 756147569f5d71672ea6175b5daa9f13e10c5695..afe795b00ab28851dc9fda41644148a01316529a 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,9 @@ Notably:
   [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
   becomes unreliable. We do not consider this an issue since we use `lia` (for
   which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* `Set Allow StrictProp`: the type of strict propositions (`SProp`) is enabled
+  by default since Coq 8.12. To make prior versions of Coq happy we need to
+  allow it explicitly.
 
 ## Prerequisites
 
diff --git a/_CoqProject b/_CoqProject
index 01aefbbf95b3dd83bbb0fcf9be5925f09c3b50f3..6ea277df73f7bcd40ab35a6bc0b7514b9d4c6e32 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,7 +5,6 @@
 theories/options.v
 theories/base.v
 theories/tactics.v
-theories/sprop.v
 theories/option.v
 theories/fin_map_dom.v
 theories/boolset.v
diff --git a/theories/base.v b/theories/base.v
index ad373c01bc50804cd42e3ff8d973aaaed35964ea..b8bc0b8fc91594aa065c54f6b7ad6193e7924c8c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,6 +10,7 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
+From Coq Require Export Logic.StrictProp.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 From stdpp Require Import options.
@@ -49,6 +50,10 @@ Obligation Tactic := idtac.
 (** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
+(** 4. [StrictProp] is enabled by default since Coq 8.12. To make prior versions
+of Coq happy we need to allow it explicitly. *)
+Global Set Allow StrictProp.
+
 (** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
@@ -645,6 +650,21 @@ Proof. destruct b; simpl; tauto. Qed.
 Lemma Is_true_false (b : bool) : b = false → ¬b.
 Proof. now intros -> ?. Qed.
 
+(** ** SProp *)
+Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
+Proof.
+  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
+  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
+Qed.
+
+Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
+
+Lemma SIs_true_intro b : Is_true b → SIs_true b.
+Proof. apply squash. Qed.
+Lemma SIs_true_elim b : SIs_true b → Is_true b.
+Proof. apply unsquash. destruct b; [left|right]; simpl; tauto. Qed.
+
+
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
 Global Instance unit_equivalence : Equivalence (≡@{unit}).
diff --git a/theories/numbers.v b/theories/numbers.v
index 13e32b54a114e4d81359de124edb8f86deadb1dc..4c15f5a87029de829d71af737fba517bfafa13dc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -3,7 +3,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
-From stdpp Require Export base decidable option sprop.
+From stdpp Require Export base decidable option.
 From stdpp Require Import options.
 Local Open Scope nat_scope.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index 16425021b435d1f821ba2a9dcc6298a7ba08b58c..a57840b174ffa5ae2e10ddf6dd4b974cdb400fa5 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -8,7 +8,6 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
-From stdpp Require Export sprop.
 From stdpp Require Import options.
 
 Local Open Scope positive_scope.
diff --git a/theories/sprop.v b/theories/sprop.v
deleted file mode 100644
index f2c68709cab620272e29b568196722d24029dafd..0000000000000000000000000000000000000000
--- a/theories/sprop.v
+++ /dev/null
@@ -1,20 +0,0 @@
-From Coq Require Export Logic.StrictProp.
-From stdpp Require Import decidable.
-From stdpp Require Import options.
-
-(** [StrictProp] is enabled by default since Coq 8.12. To make prior versions
-of Coq happy we need to allow it explicitly. *)
-Global Set Allow StrictProp.
-
-Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
-Proof.
-  intros HP. destruct (decide P) as [?|HnotP]; [assumption|].
-  assert sEmpty as []. destruct HP. destruct HnotP; assumption.
-Qed.
-
-Definition SIs_true (b : bool) : SProp := Squash (Is_true b).
-
-Lemma SIs_true_intro b : Is_true b → SIs_true b.
-Proof. apply squash. Qed.
-Lemma SIs_true_elim b : SIs_true b → Is_true b.
-Proof. apply (unsquash _). Qed.