Fix compile for architectures other than AArch64 (#192)

Some changes were not correctly propagated to all architectures.

1 files changed, 2 insertions, 2 deletions

diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 334bedf6..c57d3652 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -835,7 +835,7 @@ Proof.
   assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)).
   { constructor; auto. }
   exploit eval_mullhs. try apply HELPERS. eexact A0. instantiate (1 := Int64.repr M).  intros (v1 & A1 & B1).
-  exploit eval_addl. try apply HELPERS. eexact A1. eexact A0. intros (v2 & A2 & B2).
+  exploit eval_addl. auto. eexact A1. eexact A0. intros (v2 & A2 & B2).
   exploit eval_shrluimm. try apply HELPERS. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3).
   set (a4 := if zlt M Int64.half_modulus
              then mullhs (Eletvar 0) (Int64.repr M)
@@ -844,7 +844,7 @@ Proof.
   assert (A4: eval_expr ge sp e m le a4 v4).
   { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. }
   exploit eval_shrlimm. try apply HELPERS. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5).
-  exploit eval_addl. try apply HELPERS. eexact A5. eexact A3. intros (v6 & A6 & B6).
+  exploit eval_addl. auto. eexact A5. eexact A3. intros (v6 & A6 & B6).
   assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true).
   { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
     assert (64 < Int.max_unsigned) by (compute; auto). omega. }