test-suite/bugs/closed/5618.v


1
2
3
4
5
6
7
8
9

Require Import FunInd.

Function test {T} (v : T) (x : nat) : nat :=
  match x with
  | 0 => 0
  | S x' => test v x'
  end.

Check R_test_complete.