aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Framework
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-08 01:45:55 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-08 01:45:55 -0500
commit4c1f3132fc077c2e33ec94f20674e7c4cf714f68 (patch)
tree9cd6a61bcdd380ef58e288cb51bdcb9630e2ebd4 /src/Specific/Framework
parentf5f0e769f7af6c118df6d821898dc160a0d4b3f8 (diff)
Fix another side condition issue
Diffstat (limited to 'src/Specific/Framework')
-rw-r--r--src/Specific/Framework/ArithmeticSynthesis/Freeze.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
index 7fd723cb8..8c291bc1c 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
@@ -58,8 +58,7 @@ Section gen.
let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
presolve_op_F constr:(wt) x;
[ autorewrite with pattern_runtime; reflexivity | ].
- rewrite eval_freeze with (c := c);
- try eassumption; try omega; try reflexivity.
+ reflexivity.
Defined.
End gen.