Fix RulesProofs

JasonGross · Jan 22, 2024 · fc15137 · fc15137
1 parent fb1314d
commit fc15137
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
@@ -587,11 +587,6 @@ Proof using Type.
   all: repeat interp_good_t_step_arith.
   all: remove_casts; try fin_with_nia.
   all: try (reflect_hyps; lia).
-
-  { (* cmov c 0 -1 -> sbb 0 0 c *)
-    enough (- c mod (M + 1) = M) as E by (rewrite E; remove_casts; trivial).
-    match goal with H5 : _ |- _ => apply unfold_is_bounded_by_bool in H5; cbn in H5 end.
-    rewrite Z.mod_opp_l_nz; rewrite ?Z.mod_small; nia. }
 Qed.
 
 Lemma relaxed_rules_work rland rm1 rv v :