aboutsummaryrefslogtreecommitdiffstats
path: root/x86/Asm.v
diff options
context:
space:
mode:
Diffstat (limited to 'x86/Asm.v')
-rw-r--r--x86/Asm.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/x86/Asm.v b/x86/Asm.v
index 33f1f2ad..799b533e 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -1193,7 +1193,7 @@ Ltac Equalities :=
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros; inv H; simpl.
- omega.
+ lia.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)