From 61bd4cf7b75a51912cb885dd3b1d2ef2f7dae1e9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 2 Oct 2016 18:44:32 +0200 Subject: Finish the proofs of SelectLong for IA32 --- backend/SplitLongproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/SplitLongproof.v') 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 -> -- cgit