Commit cd53abd2 authored by Gregory Malecha's avatar Gregory Malecha
Browse files

Make [tele_arg_cons] cumulative.

parent 6e699f67
Pipeline #62980 failed with stage
in 4 minutes and 36 seconds
......@@ -35,7 +35,7 @@ Global Arguments tele_fold {_ _ !_} _ _ _ /.
(** A duplication of the type [sigT] to avoid any connection to other universes
*)
Record tele_arg_cons [X : Type] (f : X -> Type) : Type := _TargS
Cumulative Record tele_arg_cons [X : Type] (f : X -> Type) : Type := _TargS
{ head : X;
rest : f head }.
Global Arguments _TargS [X] _.
......
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