1 files changed, 0 insertions, 27 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
deleted file mode 100644
index a6ce4de0..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2083.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Require Import Program Arith.
-
-Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
-  (H : forall (i : { i | i < n }), i < p -> P i = true)
-  {measure (n - p)} :
-  Exc (forall (p : { i | i < n}), P p = true) :=
-  match le_lt_dec n p with
-  | left _ => value _
-  | right cmp =>
-      if dec (P p) then
-        check_n n P (S p) _
-      else
-        error
-  end.
-
-Require Import Omega.
-
-Solve Obligations using program_simpl ; auto with *; try omega.
-
-Next Obligation.
-  apply H. simpl. omega.
-Defined.
-
-Next Obligation. 
-  case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
-  revert H0. clear_subset_proofs. auto.
-  apply H. simpl. assumption. Defined.