From 3bab78ba755bceea93553e48654b1c50de557a5e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 12 Nov 2020 13:15:34 +0100
Subject: [PATCH] Type annotation to avoid ambigious use of `pretty`.

---
 theories/utils/switch.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index 1e2d61e..f4b820a 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -36,7 +36,7 @@ Proof.
 Qed.
 
 Lemma lookup_map_string_seq_None {A} y j z (vs : list A) :
-  (∀ i, y +:+ pretty i ≠ z) →
+  (∀ i : nat, y +:+ pretty i ≠ z) →
   map_string_seq y j vs !! z = None.
 Proof.
   intros. revert j. induction vs as [|v vs IH]=> j //=.
-- 
GitLab