Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
new file mode 100644
index 00000000..a6ce4de0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -0,0 +1,27 @@
+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.