Commit 18e02fe6 authored by Gregory Malecha's avatar Gregory Malecha
Browse files

Disable cumulativity.

parent 455f5701
Pipeline #62999 canceled with stage
in 2 minutes and 13 seconds
......@@ -5,7 +5,7 @@ Local Set Universe Polymorphism.
Local Unset Universe Minimization ToSet.
(** Telescopes *)
Cumulative Inductive tele : Type :=
Inductive tele : Type :=
| TeleO : tele
| TeleS {X} (binder : X tele) : tele.
......@@ -35,7 +35,7 @@ Global Arguments tele_fold {_ _ !_} _ _ _ /.
(** A duplication of the type [sigT] to avoid any connection to other universes
*)
Cumulative Record tele_arg_cons (X : Type) (f : X -> Type) : Type := TeleArgCons
Record tele_arg_cons (X : Type) (f : X -> Type) : Type := TeleArgCons
{ tele_arg_head : X;
tele_arg_tail : f tele_arg_head }.
Global Arguments tele_arg_cons [_] _.
......
Supports Markdown
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