diff options
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 2aed0cdf..04afe4da 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1974,7 +1974,7 @@ Ltac NOTIN := exploit tr_simple_rvalue; eauto. simpl; intro SL1. subst sl0; simpl Kseqlist. econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. apply S. eapply tr_expr_monotone; eauto. @@ -1996,7 +1996,7 @@ Ltac NOTIN := auto. + (* for effects *) econstructor; split. - right; split. apply star_refl. simpl. apply plus_lt_compat_r. + right; split. apply star_refl. simpl. apply Nat.add_lt_mono_r. apply (leftcontext_size _ _ _ H). simpl. lia. econstructor; eauto. exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1. |