diff options
| -rw-r--r-- | backend/CSE3analysisproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 4c6b417c..b298ea65 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1053,7 +1053,7 @@ Section SOUNDNESS. unfold store2. intros. destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. - Admitted. + Qed. Hint Resolve store2_sound : cse3. |