test-suite/bugs/closed/shouldsucceed/1718.v


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.