Skip to content
Snippets Groups Projects
Commit 1812fac1 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Gregory Malecha
Browse files

Compatibility with Coq 8.11 (by @Blaisorblade)

parent 7d560c15
No related branches found
No related tags found
1 merge request!368Define [tele_arg] as a fixpoint
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
theories/telescopes.v
+ 2
− 1
View file @ 1812fac1
...@@ -36,9 +36,10 @@ Global Arguments tele_fold {_ _ !_} _ _ _ /. ...@@ -36,9 +36,10 @@ Global Arguments tele_fold {_ _ !_} _ _ _ /.
(** A duplication of the type [sigT] to avoid any connection to other universes (** 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; { head : X;
rest : f head }. rest : f head }.
Global Arguments tS [X] _ : assert.
(** A sigma-like type for an "element" of a telescope, i.e. the data it (** 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]. *) takes to get a [T] from a [TT -t> T]. *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment