summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
-rw-r--r--cfrontend/Cshmgenproof.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 7906944..1eb5830 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -658,8 +658,8 @@ Proof.
econstructor. eauto. econstructor. eauto. constructor.
econstructor; eauto.
apply alignof_blockcopy_1248.
- apply sizeof_pos.
- eapply Zdivide_trans. apply alignof_blockcopy_divides. apply sizeof_alignof_compat.
+ apply sizeof_pos.
+ apply sizeof_alignof_blockcopy_compat.
Qed.
Lemma make_store_correct: