blob: 7e7f2c3737a9f68c46ff5a1fd03878f2c9ef7fb1 (
plain)
1
2
3
4
5
6
7
8
|
(* Testing robustness of typing for a fixpoint with evars in its type *)
Inductive foo (n : nat) : Type := .
Definition foo_denote {n} (x : foo n) : Type := match x with end.
Definition baz : forall n (x : foo n), foo_denote x.
refine (fix go n (x : foo n) : foo_denote x := _).
Abort.
|
