test-suite/success/coqbugs0181.v


1
2
3
4
5
6
7


(* test the strength of pretyping unification *)

Require PolyList.
Definition listn := [A,n] {l:(list A)|(length l)=n}.
Definition make_ln [A,n;l:(list A); h:([l](length l)=n l)] :=
  (exist ?? l h).