aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--arm/Asmgenproof.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 25f91d23..a592e12a 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -225,7 +225,7 @@ Proof.
TailNoLabel.
eapply tail_nolabel_trans; TailNoLabel.
Qed.
-Hint Resolve indexed_memory_access_label.
+Hint Resolve indexed_memory_access_label: labels.
Remark loadind_label:
forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c.