diff options
Diffstat (limited to 'test-suite/success/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 1cf707583..b78651c91 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -21,7 +21,7 @@ Inductive Y : Set := Inductive eq1 : forall A:Type, let B:=A in A -> Prop := refl1 : eq1 True I. -Check +Check fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => let B := A in fun (a : A) (e : eq1 A a) => |