aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1718.v
blob: 715fa94199c7587b3494aa208d4ca844e8f7c3f2 (plain)
1
2
3
4
5
6
7
8
9
(* lazy delta unfolding used to miss delta on rels and vars (fixed in 10172) *)

Check
  let g := fun _ => 0 in
  fix f (n : nat) :=
  match n with
  | 0 => g f
  | S n' => 0
  end.