aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1907.v
blob: 55fc823190d09fadcc6ca6590f4a008442647d54 (plain)
1
2
3
4
5
6
7
(* An example of type inference *)

Axiom A : Type.
Definition f (x y : A) := x.
Axiom g : forall x y : A, f x y = y -> Prop.
Axiom x : A.
Check (g x _ (refl_equal x)).