From 10c81e90a836c8abea32bc6157976b9adf7775fa Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Thu, 29 Jun 2017 17:27:04 +0200
Subject: closing bug #5618 introduce by PR 828

---
 test-suite/bugs/closed/5618.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/5618.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v
new file mode 100644
index 0000000000..ab88a88f44
--- /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
-- 
cgit v1.2.3