1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index 21b8c4c..5e16f05 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -750,7 +750,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.