diff options
| -rw-r--r-- | backend/CSE2proof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 0d369e7a..0b92f5e5 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -358,6 +358,7 @@ Proof. discriminate. assumption. Qed. +Local Hint Resolve wellformed_reg_kill_mem : wellformed. Lemma wellformed_mem_move: forall r dst rel, |