Fixes in Program well-founded definitions:

- de Bruijn bug #2083
- Avoid useless eta-expansion (bug #2060)


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

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 0000000000..3e2d00cbad
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -0,0 +1,27 @@
+Require Import Program Arith.
+Set Implicit Arguments.
+
+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 (fun i => n - i) 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 (S p) _
+      else
+        error
+  end.
+
+Require Import Omega.
+
+Next Obligation.
+  apply H. simpl. omega.
+Defined.
+
+Next Obligation. 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.