diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1784.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1784.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 5855b168..718b0e86 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -56,16 +56,16 @@ Require Import Program. Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with - | I x => + | I x => match y with | I y => if (Z_eq_dec x y) then in_left else in_right | S ys => in_right end - | S xs => + | S xs => match y with | I y => in_right | S ys => - let fix list_in (xs ys:list sv) {struct xs} : + let fix list_in (xs ys:list sv) {struct xs} : {slist_in xs ys} + {~slist_in xs ys} := match xs with | nil => in_left @@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := | y::ys => if lt_dec x y then in_left else if elem_in ys then in_left else in_right end - in - if elem_in ys then + in + if elem_in ys then if list_in xs ys then in_left else in_right else in_right end @@ -90,12 +90,12 @@ Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H; subst. Defined. Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. + intro H1; contradict H. inversion H1; subst. assumption. contradict H0; assumption. Defined. Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. Next Obligation. - intro H0; contradict H. inversion H0; subst. assumption. Defined. + intro H1; contradict H. inversion H1; subst. assumption. Defined. Next Obligation. intro H0; contradict H. inversion H0; subst; auto. Defined. |