aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3808.v
blob: a5c84e6856988c379a12cbcbc1ebe0ff7c6af304 (plain)
1
2
3
Unset Strict Universe Declaration.
Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
  := foo : Foo.