diff options
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index ebf2c5ea..61a37180 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -339,7 +339,7 @@ Qed. Lemma aregs_sound: forall bc e ae rl, ematch bc e ae -> list_forall2 (vmatch bc) (e##rl) (aregs ae rl). Proof. - induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto. + induction rl; simpl; intros. constructor. constructor; [apply areg_sound|]; auto. Qed. Global Hint Resolve areg_sound aregs_sound: va. |