3808.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/3808.v

blob: ac6a8501935188cdbc569a837413dde530cb524e (plain)

1
2
3

Unset Strict Universe Declaration.
Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
  := foo : Foo.