From ae141ea08f9ae743650ee49722f97049459e40ba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 21 Dec 2018 12:29:30 -0500 Subject: Add eval_freeze_to_bytesmod to push_eval --- src/Experiments/NewPipeline/Toplevel1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Experiments/NewPipeline/Toplevel1.v') 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 -- cgit v1.2.3