diff --git a/theories/sprop.v b/theories/sprop.v
index edf9a73ca8d0a74f8e31af8c3b19579ea51540f7..1e6a0be06386f1109718477edd0054a2805601e0 100644
--- a/theories/sprop.v
+++ b/theories/sprop.v
@@ -2,6 +2,8 @@ From Coq Require Export Logic.StrictProp.
 From stdpp Require Import decidable.
 From stdpp Require Import options.
 
+Global Set Allow StrictProp.
+
 Lemma unsquash (P : Prop) `{!Decision P} : Squash P → P.
 Proof.
   intros HP. destruct (decide P) as [?|HnotP]; [assumption|].