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

summary refs log tree commit diff

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

blob: 6015c53b8a5daa0bfcf5dc471a8e029f28d4cd2e (plain)

(* Testing typing of subst *)

Lemma eqType2Set (a b : Set) (H : @eq Type a b) : @eq Set a b.
Fail subst.