From 570ea001f496e90afb7f06dc8250e67d0474c05a Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 14 Mar 2025 15:31:55 +0100
Subject: [PATCH] open your eyes; your double-blindness is cured

---
 _CoqProject        | 3 +--
 coq-simuliris.opam | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 3f81f7a4..a982889c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,7 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# Warning seems incorrect
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
 
 theories/logic/satisfiable.v
@@ -124,7 +124,6 @@ theories/stacked_borrows/examples/coinductive.v
 
 
 ## Tree Borrows
-# theories/tree_borrows/helpers.v
 theories/tree_borrows/locations.v
 theories/tree_borrows/lang_base.v
 theories/tree_borrows/notation.v
diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index 391e36d5..198a64d6 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-maintainer: "Homer Simpson <homer@simpson.org>"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
 authors: "Simuliris Authors"
 homepage: "http://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/simuliris/issues"
-- 
GitLab