aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Linearizeproof.v
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
commitf16fa31ec9cc90da750c8cc10f447023962cd153 (patch)
tree28eed4d4b5bc964907f20332d1eed470a393d07b /backend/Linearizeproof.v
parent485a4c0dd450e65745c83e59acdb40b42058e556 (diff)
parentd703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff)
downloadcompcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz
compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'backend/Linearizeproof.v')
-rw-r--r--backend/Linearizeproof.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 18dc52a5..c12eab6e 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -658,7 +658,7 @@ Proof.
- (* Lbranch *)
assert ((reachable f)!!pc = true). apply REACH; simpl; auto.
- right; split. simpl; omega. split. auto. simpl. econstructor; eauto.
+ right; split. simpl; lia. split. auto. simpl. econstructor; eauto.
- (* Lcond *)
assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto).
@@ -675,12 +675,12 @@ Proof.
rewrite eval_negate_condition. rewrite H. auto. eauto.
rewrite DC. econstructor; eauto.
(* cond is false: branch is taken *)
- right; split. simpl; omega. split. auto. rewrite <- DC. econstructor; eauto.
+ right; split. simpl; lia. split. auto. rewrite <- DC. econstructor; eauto.
rewrite eval_negate_condition. rewrite H. auto.
(* branch if cond is true *)
destruct b.
(* cond is true: branch is taken *)
- right; split. simpl; omega. split. auto. econstructor; eauto.
+ right; split. simpl; lia. split. auto. econstructor; eauto.
(* cond is false: no branch *)
left; econstructor; split.
apply plus_one. eapply exec_Lcond_false. eauto. eauto.
@@ -689,7 +689,7 @@ Proof.
- (* Ljumptable *)
assert (REACH': (reachable f)!!pc = true).
apply REACH. simpl. eapply list_nth_z_in; eauto.
- right; split. simpl; omega. split. auto. econstructor; eauto.
+ right; split. simpl; lia. split. auto. econstructor; eauto.
- (* Lreturn *)
left; econstructor; split.