From 653c819a4e55c43c54d898fc7b797f6fac9b8e1a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 16:02:21 +0200
Subject: [PATCH] fix build on Coq 8.10

---
 tests/gmap.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/gmap.v b/tests/gmap.v
index 8fdc6174..6cb7029b 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -22,14 +22,14 @@ Proof.
   Show.
 Abort.
 
-Goal 1 ∈ dom (M := gmap _ _) (gset _) (<[ 1 := 2 ]> ∅).
+Goal 1 ∈ dom (M := gmap nat nat) (gset nat) (<[ 1 := 2 ]> ∅).
 Proof.
   Fail progress simpl.
   Fail progress cbn.
   Show.
 Abort.
 
-Goal bool_decide (∅ =@{gset _} {[ 1; 2; 3 ]}) = false.
+Goal bool_decide (∅ =@{gset nat} {[ 1; 2; 3 ]}) = false.
 Proof.
   Fail progress simpl.
   Fail progress cbn.
@@ -37,7 +37,7 @@ Proof.
   reflexivity.
 Qed.
 
-Goal bool_decide (∅ ≡@{gset _} {[ 1; 2; 3 ]}) = false.
+Goal bool_decide (∅ ≡@{gset nat} {[ 1; 2; 3 ]}) = false.
 Proof.
   Fail progress simpl.
   Fail progress cbn.
@@ -45,7 +45,7 @@ Proof.
   reflexivity.
 Qed.
 
-Goal bool_decide (1 ∈@{gset _} {[ 1; 2; 3 ]}) = true.
+Goal bool_decide (1 ∈@{gset nat} {[ 1; 2; 3 ]}) = true.
 Proof.
   Fail progress simpl.
   Fail progress cbn.
@@ -53,7 +53,7 @@ Proof.
   reflexivity.
 Qed.
 
-Goal bool_decide (∅ ##@{gset _} {[ 1; 2; 3 ]}) = true.
+Goal bool_decide (∅ ##@{gset nat} {[ 1; 2; 3 ]}) = true.
 Proof.
   Fail progress simpl.
   Fail progress cbn.
@@ -61,7 +61,7 @@ Proof.
   reflexivity.
 Qed.
 
-Goal bool_decide (∅ ⊆@{gset _} {[ 1; 2; 3 ]}) = true.
+Goal bool_decide (∅ ⊆@{gset nat} {[ 1; 2; 3 ]}) = true.
 Proof.
   Fail progress simpl.
   Fail progress cbn.
-- 
GitLab