Test bug 705

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5712 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 0 deletions

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.