diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:40:02 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:40:02 +0100 |
| commit | e35365927d1289687aaff6d7ca5ebee1ac09d249 (patch) | |
| tree | 1739477bf99f1d4547b555c34c321c95dec1cfcf /backend/CSE2proof.v | |
| parent | e4c7ff447ad30832c42ee51f0fe7e1cf62d2eee9 (diff) | |
| download | compcert-kvx-e35365927d1289687aaff6d7ca5ebee1ac09d249.tar.gz compcert-kvx-e35365927d1289687aaff6d7ca5ebee1ac09d249.zip | |
add hint
Diffstat (limited to 'backend/CSE2proof.v')
| -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, |