blob: 3929fbae23696578aabede4464f1598189eeee30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Definition bug := Eval vm_compute in eq_rect.
(* bug:
Error: Illegal application (Type Error):
The term "eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"x" : "A"
"P" : "A -> Type"
"x0" : "A"
The 1st term has type "A" which should be coercible to
"Type".
*)
|
