From 362b7ef4422b451e621ca8400692de1decb0503d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 14:08:04 +0100
Subject: Test for bug #3490.

---
 test-suite/bugs/closed/3490.v | 27 +++++++++++++++++++++++++++
 test-suite/bugs/opened/3490.v | 27 ---------------------------
 2 files changed, 27 insertions(+), 27 deletions(-)
 create mode 100644 test-suite/bugs/closed/3490.v
 delete mode 100644 test-suite/bugs/opened/3490.v

diff --git a/test-suite/bugs/closed/3490.v b/test-suite/bugs/closed/3490.v
new file mode 100644
index 0000000000..e7a5caa1de
--- /dev/null
+++ b/test-suite/bugs/closed/3490.v
@@ -0,0 +1,27 @@
+Inductive T : Type :=                                                                                        
+| Var : nat -> T                                                                                                 
+| Arr : T -> T -> T.                                                                                             
+
+Inductive Tele : list T -> Type :=                                                                               
+| Tnil  : @Tele nil                                                                                              
+| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
+
+Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
+   : { x : Type & x -> nat -> Type } :=
+     match t return { x : Type & x -> nat -> Type } with
+       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
+       | Tcons ls t' l =>
+         let (result, get) := TeleD ls t' in
+         @existT Type (fun x => x -> nat -> Type)
+                 { v : result & (fix TD (t : T) {struct t} :=
+                                   match  t with
+                                     | Var n =>
+                                       get v n
+                                     | Arr a b => TD a -> TD b
+                                   end) l }
+                 (fun x n =>
+                    match n return Type with
+                      | 0 => projT2 x
+                      | S n => get (projT1 x) n
+                    end)
+     end.
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v
deleted file mode 100644
index e7a5caa1de..0000000000
--- a/test-suite/bugs/opened/3490.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Inductive T : Type :=                                                                                        
-| Var : nat -> T                                                                                                 
-| Arr : T -> T -> T.                                                                                             
-
-Inductive Tele : list T -> Type :=                                                                               
-| Tnil  : @Tele nil                                                                                              
-| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
-
-Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
-   : { x : Type & x -> nat -> Type } :=
-     match t return { x : Type & x -> nat -> Type } with
-       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
-       | Tcons ls t' l =>
-         let (result, get) := TeleD ls t' in
-         @existT Type (fun x => x -> nat -> Type)
-                 { v : result & (fix TD (t : T) {struct t} :=
-                                   match  t with
-                                     | Var n =>
-                                       get v n
-                                     | Arr a b => TD a -> TD b
-                                   end) l }
-                 (fun x n =>
-                    match n return Type with
-                      | 0 => projT2 x
-                      | S n => get (projT1 x) n
-                    end)
-     end.
-- 
cgit v1.2.3