diff options
author | jadep <jadep@mit.edu> | 2019-02-15 13:10:00 -0500 |
---|---|---|
committer | jadep <jadep@mit.edu> | 2019-02-15 13:14:09 -0500 |
commit | 5ada7bb4874a2ddcc75ba72bbbfbc5f2c3864645 (patch) | |
tree | 8d40f0a606c74a76f698926bec7b6f6c40f5bbbb /src | |
parent | b06d11d9e12cae00475e8f9a5f69d42cf34ae729 (diff) |
Fix missing "= true" in a tactic so [Admitted] is unneccesary.
Co-authored-by: Jason Gross <jgross@mit.edu>
Diffstat (limited to 'src')
-rw-r--r-- | src/RewriterRulesInterpGood.v | 6 |
1 files 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. |