blob: dee321c0279bef7ae4745dad35f9ced989531bbf (
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.
|
