From fde847543e8169082db0138a9713a8c0ab0cc167 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 30 Jun 2020 12:44:23 +0200 Subject: Added missing hint database name. --- arm/Asmgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm') 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. -- cgit