From 5ada7bb4874a2ddcc75ba72bbbfbc5f2c3864645 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 15 Feb 2019 13:10:00 -0500 Subject: Fix missing "= true" in a tactic so [Admitted] is unneccesary. Co-authored-by: Jason Gross --- src/RewriterRulesInterpGood.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 612f72afd..8654def0d 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -679,9 +679,9 @@ Module Compilers. clear H; rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1)) in * by assumption end - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) |- context[ident.cast ?coor ?r ?v] ] + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast ?coor ?r ?v] ] => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption - | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r), H' : context[ident.cast ?coor ?r ?v] |- _ ] + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true, H' : context[ident.cast ?coor ?r ?v] |- _ ] => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r r[0~>?x-1]%zrange = true, @@ -784,7 +784,7 @@ Module Compilers. Time all: fancy_local_t. (* Finished transaction in 0.051 secs (0.052u,0.s) (successful) *) Time all: systematically_handle_casts. (* Finished transaction in 2.004 secs (1.952u,0.052s) (successful) *) Time all: try solve [ repeat interp_good_t_step_arith ]. (* Finished transaction in 44.411 secs (44.004u,0.411s) (successful) *) - Admitted. + Qed. End with_cast. End RewriteRules. End Compilers. -- cgit v1.2.3