diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:43:52 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:43:52 +0100 |
| commit | a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a (patch) | |
| tree | 8fa2727d9ec0b968674caf76a38dccc50947a6d1 /backend/ForwardMovesproof.v | |
| parent | fb5029eb72a3a28b26f3d982c30badc8d027f405 (diff) | |
| download | compcert-kvx-a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a.tar.gz compcert-kvx-a8dd20cd96a1c8636add5b8b45b6ee5ff5982f9a.zip | |
fix move
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 8e2ba9af..b1425401 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -470,8 +470,10 @@ Proof. simpl in H0. destruct (map # pc') as [mpc' | ] in *; try discriminate. simpl in GE. - unfold move in GE. + admit. + admit. } + admit. (* load *) - econstructor; split. |