aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmgenproof.v')
-rw-r--r--aarch64/Asmgenproof.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index d3515a96..dc0bc509 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
Proof.
intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
- omega.
+ lia.
Qed.
Lemma exec_straight_exec:
@@ -424,8 +424,8 @@ Proof.
split. unfold goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
- auto. omega.
- generalize (transf_function_no_overflow _ _ H0). omega.
+ auto. lia.
+ generalize (transf_function_no_overflow _ _ H0). lia.
intros. apply Pregmap.gso; auto.
Qed.
@@ -949,10 +949,10 @@ Local Transparent destroyed_by_op.
rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
reflexivity.
eexact U. }
- exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+ exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
intros (ofs' & X & Y).
left; exists (State rs3 m3'); split.
- eapply exec_straight_steps_1; eauto. omega. constructor.
+ eapply exec_straight_steps_1; eauto. lia. constructor.
econstructor; eauto.
rewrite X; econstructor; eauto.
apply agree_exten with rs2; eauto with asmgen.
@@ -981,7 +981,7 @@ Local Transparent destroyed_at_function_entry. simpl.
- (* return *)
inv STACKS. simpl in *.
- right. split. omega. split. auto.
+ right. split. lia. split. auto.
rewrite <- ATPC in H5.
econstructor; eauto. congruence.
Qed.