aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2135.v
blob: 61882176aa81b19a3379def1a21528d1c4cb47b2 (plain)
1
2
3
4
5
6
7
8
9
(* Check that metas are whd-normalized before trying 2nd-order unification *)
Lemma test : 
  forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop),
  (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A))
  -> Q D (T D).
Proof.
  intros D T Q H.
  pattern (T D). apply H.
Qed.