aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/coqbugs0181.v
blob: d541dcf7b0757e04999c9d7f0d8759de21cf12f6 (plain)
1
2
3
4
5
6
7

(* test the strength of pretyping unification *)

Require Import List.
Definition listn A n := {l : list A | length l = n}.
Definition make_ln A n (l : list A) (h : (fun l => length l = n) l) :=
  exist _ l h.