From 62778753dd39a1e70b05d86ee4b75058ce788dbd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 29 Apr 2004 17:36:07 +0000
Subject: Test bug 705

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5712 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/evars.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index a7b6d6d83c..6c168f4720 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -21,3 +21,16 @@ Definition f1 [frm0,a1]: B := (f frm0 a1).
 (* Checks that solvable ? in the type part of the definition are harmless *)
 Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1).
 
+(* Checks that sorts that are evars are handled correctly (bug 705) *)
+Require PolyList.
+
+Fixpoint build [nl : (list nat)] :
+ (Cases nl of nil => True | _ => False end) -> unit :=
+ <[nl](Cases nl of nil => True | _ => False end) -> unit>Cases nl of
+ | nil => [_]tt
+ | (cons n rest) =>
+   Cases n of
+   | O => [_]tt
+   | (S m) => [a](build rest (False_ind ? a))
+   end
+  end.
-- 
cgit v1.2.3