From 3494dfbaa916bde1d8e31a1e2331dabaab493a92 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Oct 2020 18:43:39 +0200
Subject: [PATCH] fix strange scope error with Coq 8.10
---
theories/algebra/lib/gmap_view.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index a3a7b544f..55f3962a1 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -205,7 +205,7 @@ Section lemmas.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_valid. setoid_rewrite gmap_view_rel_lookup.
split; intros Hm; split.
- - apply (Hm 0).
+ - apply (Hm 0%nat).
- apply equiv_dist=>n. apply Hm.
- apply Hm.
- revert n. apply equiv_dist. apply Hm.
--
GitLab