diff options
| -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. |