diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index c10b8ac2..b3895768 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -419,8 +419,7 @@ Lemma transfer_regs_dead inputs rs r: ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef. Proof. unfold transfer_regs; induction inputs; simpl; intuition subst. - - rewrite Regmap.gi; auto. - - rewrite Regmap.gso; auto. + rewrite Regmap.gso; auto. Qed. Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t := |