diff options
Diffstat (limited to 'src/hls/IfConversionproof.v')
| -rw-r--r-- | src/hls/IfConversionproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index 2d8cfac..f24a4c4 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -697,7 +697,7 @@ Section CORRECTNESS. - destruct_match. inv Heqp1. simplify. unfold not in *. destruct (peq p1 p0); subst; try solve [exfalso; auto]. - unfold eval_predf. simplify. rewrite ! Pos2Nat.id. + unfold eval_predf. simplify. rewrite ! Regmap.gso; auto. - rewrite eval_predf_Pand in *. assert ((~ In p0 (predicate_use p1_1)) /\ (~ In p0 (predicate_use p1_2))). |