From fd23a783ae213845282803d935c74f794d0e4d09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 23:06:18 +0200
Subject: [PATCH] `Set Allow StrictProp` to make CI happy.

---
 theories/sprop.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/sprop.v b/theories/sprop.v
index edf9a73c..1e6a0be0 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|].
-- 
GitLab