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: 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.