diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-21 12:29:30 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-21 12:30:43 -0500 |
| commit | ae141ea08f9ae743650ee49722f97049459e40ba (patch) | |
| tree | 91e381a80e26df35ee9f145828dd5d379d850986 /src/Experiments/NewPipeline/Toplevel1.v | |
| parent | ae1dd5ee0cc7f86690182c01a13f6a522343a549 (diff) | |
Add eval_freeze_to_bytesmod to push_eval
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 957264d3f..b1eee614e 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -1885,7 +1885,7 @@ Module Import UnsaturatedSolinas. { apply Hto_bytesv; solve [ assumption | repeat split ]. } { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *. rewrite Bool.andb_true_iff in *; split_and'. - etransitivity; [ apply eval_freeze_to_bytesmod | f_equal; (eassumption || (symmetry; eassumption)) ]; + etransitivity; [ apply eval_freeze_to_bytesmod_and_partitions | f_equal; (eassumption || (symmetry; eassumption)) ]; auto; try omega. { erewrite Ring.length_is_bounded_by by eassumption; assumption. } { lazymatch goal with |