diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-21 18:22:00 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 15:29:56 +0100 |
| commit | aba0e740f25ffa5c338dfa76cab71144802cebc2 (patch) | |
| tree | 746115009aa60b802a2b5369a5106a2e971eb22f /cfrontend/SimplExprproof.v | |
| parent | 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 (diff) | |
| download | compcert-kvx-aba0e740f25ffa5c338dfa76cab71144802cebc2.tar.gz compcert-kvx-aba0e740f25ffa5c338dfa76cab71144802cebc2.zip | |
Replace `omega` tactic with `lia`
Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.
Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.
Turn back on the deprecation warning for uses of `omega`.
Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 9a3f32ec..2d059ddd 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1449,13 +1449,13 @@ Proof. (* for val *) intros [SL1 [TY1 EV1]]. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_val_val; auto. (* for effects *) intros SL1. subst sl. econstructor; split. - right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + right; split. apply star_refl. destruct r; simpl; (contradiction || lia). econstructor; eauto. instantiate (1 := tmps). apply tr_top_base. constructor. (* for set *) @@ -1779,7 +1779,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1788,7 +1788,7 @@ Proof. subst; simpl Kseqlist. econstructor; split. right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. - simpl. omega. + simpl. lia. constructor. (* postincr *) exploit tr_top_leftcontext; eauto. clear H14. @@ -1846,7 +1846,7 @@ Proof. subst. simpl Kseqlist. econstructor; split. right; split. rewrite app_ass; rewrite Kseqlist_app. eexact EXEC. - simpl; omega. + simpl; lia. constructor. (* for value *) exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. @@ -1863,7 +1863,7 @@ Proof. subst sl0; simpl Kseqlist. econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. auto. auto. @@ -1885,7 +1885,7 @@ Proof. (* for effects *) econstructor; split. right; split. apply star_refl. simpl. apply plus_lt_compat_r. - apply (leftcontext_size _ _ _ H). simpl. omega. + apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. apply S. constructor; auto. auto. auto. @@ -2015,12 +2015,12 @@ Proof. inv H6. inv H0. econstructor; split. right; split. apply push_seq. - simpl. omega. + simpl. lia. econstructor; eauto. constructor. auto. (* do 2 *) inv H7. inv H6. inv H. econstructor; split. - right; split. apply star_refl. simpl. omega. + right; split. apply star_refl. simpl. lia. econstructor; eauto. constructor. (* seq *) |