diff options
Diffstat (limited to 'backend/CastOptimproof.v')
| -rw-r--r-- | backend/CastOptimproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v index d507609..b04e061 100644 --- a/backend/CastOptimproof.v +++ b/backend/CastOptimproof.v @@ -118,7 +118,7 @@ Proof. intros approxs; intros. apply regs_match_approx_increasing with (transfer f pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. auto. intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. |