diff options
Diffstat (limited to 'cfrontend/Clight.v')
| -rw-r--r-- | cfrontend/Clight.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8ab29fe9..239ca370 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -739,7 +739,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; simpl; intros. inv H; simpl; try omega. + red; simpl; intros. inv H; simpl; try lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. |