diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 18:44:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 18:44:32 +0200 |
| commit | 61bd4cf7b75a51912cb885dd3b1d2ef2f7dae1e9 (patch) | |
| tree | 87ced580a7803689125f3fc12d2a5ec657adf959 /backend/SplitLongproof.v | |
| parent | f21a6b181dded86ef0e5c7ab94f74e5b960fd510 (diff) | |
| download | compcert-kvx-61bd4cf7b75a51912cb885dd3b1d2ef2f7dae1e9.tar.gz compcert-kvx-61bd4cf7b75a51912cb885dd3b1d2ef2f7dae1e9.zip | |
Finish the proofs of SelectLong for IA32
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 57fc6b56..a10ee3f7 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -876,7 +876,7 @@ Proof. econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_divsu_base: +Theorem eval_divls_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> |