1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 63149aa..e2176fd 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -848,7 +848,7 @@ Ltac Equalities :=
   exploit external_call_determ. eexact H3. eexact H8. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
 (* trace length *)
-  inv H; simpl.
+  red; intros; inv H; simpl.
   omega.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.