From 7bd5d66520bfae2bdef6573a40798a5d6375be79 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 20 Mar 2019 11:30:21 +0100 Subject: Proving eval_divs_base --- backend/SelectDivproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/SelectDivproof.v') diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 3fd50b76..9b99fcbf 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -702,7 +702,7 @@ Proof. || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. - + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). + + exploit (eval_shrximm prog sp e m (Vint i :: le) (Eletvar O)). constructor. simpl; eauto. eapply Val.divs_pow2; eauto. intros [v1 [X LD]]. inv LD. econstructor; split. econstructor. eauto. -- cgit