From 1812fac14d4d32be39731630e3ef7e4b9a567216 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 2 Mar 2022 13:14:21 +0000
Subject: [PATCH] Compatibility with Coq 8.11 (by @blaisorblade)
---
theories/telescopes.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 14f440b1..2f148092 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -36,9 +36,10 @@ Global Arguments tele_fold {_ _ !_} _ _ _ /.
(** A duplication of the type [sigT] to avoid any connection to other universes
*)
-Record tS [X : Type] (f : X -> Type) : Type :=
+Record tS {X : Type} (f : X -> Type) : Type :=
{ head : X;
rest : f head }.
+Global Arguments tS [X] _ : assert.
(** A sigma-like type for an "element" of a telescope, i.e. the data it
takes to get a [T] from a [TT -t> T]. *)
--
GitLab