Remove useless assumptions

1 files changed, 0 insertions, 1 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 872cc2be0..9b344a577 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -738,7 +738,6 @@ Module Compilers.
 
       Lemma fancy_rewrite_rules_interp_good
             (invert_low invert_high : Z -> Z -> option Z)
-            (value_range flag_range : zrange)
             (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
             (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
         : rewrite_rules_interp_goodT fancy_rewrite_rules.