From 0e607967501c2371dfea6867338940ba06252b0c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 17:59:37 +0200
Subject: [PATCH] Add ssreflect file (from Iris).

---
 _CoqProject       |  1 +
 stdpp/ssreflect.v | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 stdpp/ssreflect.v

diff --git a/_CoqProject b/_CoqProject
index 2dfd79d4..567c5dd8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ stdpp/nat_cancel.v
 stdpp/namespaces.v
 stdpp/telescopes.v
 stdpp/binders.v
+stdpp/ssreflect.v
 
 stdpp_unstable/bitblast.v
 stdpp_unstable/bitvector.v
diff --git a/stdpp/ssreflect.v b/stdpp/ssreflect.v
new file mode 100644
index 00000000..0361cc01
--- /dev/null
+++ b/stdpp/ssreflect.v
@@ -0,0 +1,14 @@
+(** This file provides support for using std++ in combination with the ssreflect
+tactics. It patches up some global options of ssreflect. *)
+From Coq.ssr Require Export ssreflect.
+From stdpp Require Export prelude.
+From stdpp Require Import options.
+
+(** Restore Coq's normal "if" scope, ssr redefines it. *)
+Global Open Scope general_if_scope.
+
+(** See Coq issue #5706 *)
+Global Set SsrOldRewriteGoalsOrder.
+
+(** Overwrite ssr's [done] tactic with ours *)
+Ltac done := stdpp.tactics.done.
-- 
GitLab