From ee1d6bed2465c5272a14c33e7192b0ce69996e76 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 23 Jul 2024 11:26:51 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 Makefile.coq.local | 3 ++-
 tests/iprop.v      | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 4df3f5c55..f59fc80d8 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -29,7 +29,8 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
 # These versions of Coq are known to have different output so we don't test them.
 # Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
 # Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
+#COQ_NOREF= $(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
+COQ_NOREF= $(shell echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
diff --git a/tests/iprop.v b/tests/iprop.v
index edfb91062..15bbc7062 100644
--- a/tests/iprop.v
+++ b/tests/iprop.v
@@ -2,7 +2,7 @@
 of [gFunctors]:
 See [!782](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782) *)
 
-From Coq Require Import Logic.Eqdep.
+From Coq.Logic Require Import Eqdep.
 
 (** A [sigT] that is partially applied and template-polymorphic causes universe
 inconsistency errors, which is why [sigT] should be avoided for the definition
-- 
GitLab