1 files changed, 2 insertions, 77 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 49abc7c7..dd4cfa69 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -407,6 +407,7 @@ Proof.
 - InvEval. apply eval_andlimm; auto.
 - (*andn*) InvEval. TrivialExists. simpl. congruence.
 - (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence.
+  (*
 - (* selectl *)
   InvEval.
   predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; TrivialExists.
@@ -424,7 +425,7 @@ Proof.
       destruct y; simpl; trivial.
       rewrite Int64.and_commut. rewrite Int64.and_mone. reflexivity.
   + constructor. econstructor. constructor. econstructor. constructor. econstructor. constructor. eassumption. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. eassumption. constructor.
-  + simpl in *. congruence.
+  + simpl in *. congruence. *)
 - TrivialExists.
 Qed.
 
@@ -525,82 +526,6 @@ Proof.
       rewrite Int64.and_zero.
       rewrite Int64.or_zero.
       reflexivity.
-      (*
-  - (* selectl unsigned *)
-    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
-    inv H.
-    inv H0.
-    inv H6.
-    inv H3.
-    inv H2.
-    inv H7.
-    inv H4.
-    inv H3.
-    inv H6.
-    inv H4.
-    inv H3.
-    inv H14.
-    inv H13.
-    inv H6.
-    inv H4.
-    inv H13.
-    inv H14.
-    inv H9.
-    inv H11.
-    inv H13.
-    inv H3.
-    inv H6.
-    inv H7.
-    inv H3.
-    inv H14.
-    inv H17.
-    simpl in *.
-    inv H8.
-    inv H5.
-    inv H10.
-    inv H12.
-    inv H15.
-    inv H16.
-    inv H11.
-    inv H13.
-    unfold same_expr_pure in PURE.
-    destruct y0; try congruence.
-    destruct y1; try congruence.
-    destruct (ident_eq i i0); try congruence; clear PURE.
-    rewrite <- e0 in *; clear e0.
-    inv H6.
-    inv H7.
-    rename v10 into vtest.
-    replace v11 with vtest in * by congruence.
-    TrivialExists.
-    simpl.
-    f_equal.
-    unfold selectl.
-    destruct vtest; simpl; trivial.
-    rewrite Val.andl_commut.
-    destruct v4; simpl; trivial.
-    rewrite Val.andl_commut.
-    rewrite Val.orl_commut.
-    destruct v9; simpl; trivial.
-    rewrite int64_eq_commut.
-    destruct (Int64.eq i1 Int64.zero); simpl.
-    
-    + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_commut.
-      rewrite Int64.or_zero.
-      reflexivity.
-   + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_zero.
-      reflexivity.
-   +  *)
 - TrivialExists.
 Qed.