diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 714468a..1dad518 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -106,7 +106,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. |