diff options
| -rw-r--r-- | backend/SelectDiv.vp | 8 | ||||
| -rw-r--r-- | backend/SelectDivproof.v | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index d91797c5..e1ba0bff 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -178,8 +178,8 @@ Definition divsimm (e1: expr) (n2: int) := divs_base e1 (Eop (Ointconst n2) Enil) else match divs_mul_params (Int.signed n2) with - | None => divs_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (divs_mul p m) + | _ => divs_base e1 (Eop (Ointconst n2) Enil) + (* | Some(p, m) => Elet e1 (divs_mul p m) *) (* FIXME - hack K1 *) end end. @@ -204,8 +204,8 @@ Definition modsimm (e1: expr) (n2: int) := mods_base e1 (Eop (Ointconst n2) Enil) else match divs_mul_params (Int.signed n2) with - | None => mods_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) + | _ => mods_base e1 (Eop (Ointconst n2) Enil) + (* | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) *) (* FIXME - hack K1 *) end end. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 75713289..aa6750ed 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -660,9 +660,9 @@ Proof. + eapply eval_divs_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_divs_base; eauto. EvalOp. - + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. + econstructor; eauto. eapply eval_divs_mul; eauto. *) (* FIXME - hack K1 *) * eapply eval_divs_base; eauto. EvalOp. Qed. @@ -709,11 +709,11 @@ Proof. + eapply eval_mods_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. - + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * econstructor; split. econstructor. eauto. apply eval_mod_from_div with (x := i); auto. eapply eval_divs_mul with (x := i); eauto. - simpl. auto. + simpl. auto. *) (* FIXME - hack K1 *) * eapply eval_mods_base; eauto. EvalOp. Qed. |