diff options
Diffstat (limited to 'backend/Coloringproof.v')
| -rw-r--r-- | backend/Coloringproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index 5f035b4..bb97c87 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -719,7 +719,9 @@ Proof. elim (andb_prop _ _ H1); intros. caseEq (Regset.mem r allregs); intro. generalize (check_coloring_3_correct _ _ _ r H3 H4). tauto. - case (env r); simpl; intuition congruence. + case (env r); simpl. + unfold dummy_int_reg. intuition congruence. + unfold dummy_float_reg. intuition congruence. Qed. Lemma alloc_of_coloring_correct_4: |