diff options
| author |  Julien Forest <forest@ensiie.fr> | 2017-06-29 17:27:04 +0200 |
|---|---|---|
| committer | Julien Forest <forest@ensiie.fr> | 2017-06-29 17:27:04 +0200 |
| commit | 10c81e90a836c8abea32bc6157976b9adf7775fa (patch) | |
| tree | a7c4f13cacb5ea4438ba3e062f45c8fd2f15b270 /test-suite/bugs/closed/5618.v | |
| parent | 181cb78d09ba55c7a6d62b333b26595a4fbb360a (diff) | |
closing bug #5618 introduce by PR 828
Diffstat (limited to 'test-suite/bugs/closed/5618.v')
| -rw-r--r-- | test-suite/bugs/closed/5618.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v new file mode 100644 index 000000000..ab88a88f4 --- /dev/null +++ b/test-suite/bugs/closed/5618.v @@ -0,0 +1,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.
\ No newline at end of file |