From aa4b0596761658fbf452da6e955b7ef81c720387 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 May 2023 09:04:28 +0200
Subject: [PATCH] Update prelude file to use new ssreflect file from std++.

---
 iris/prelude/prelude.v | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/iris/prelude/prelude.v b/iris/prelude/prelude.v
index 8c458361c..cf8da5882 100644
--- a/iris/prelude/prelude.v
+++ b/iris/prelude/prelude.v
@@ -1,13 +1,5 @@
-From Coq.ssr Require Export ssreflect.
-From stdpp Require Export prelude.
+From stdpp Require Export ssreflect.
 From iris.prelude Require Import options.
-Global Open Scope general_if_scope.
-Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
-Ltac done := stdpp.tactics.done.
 
 (** Iris itself and many dependencies still rely on this coercion. *)
 Coercion Z.of_nat : nat >-> Z.
-
-(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
-fixed in Coq >= 8.12, which Iris depends on. *)
-Global Hint Mode Equiv ! : typeclass_instances.
-- 
GitLab