diff options
Diffstat (limited to 'backend/CSE2proof.v')
-rw-r--r-- | backend/CSE2proof.v | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index e62e2ae6..3799e38b 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -317,14 +317,9 @@ Proof. specialize Hrel with (i := i) (j := j) (sv := sv). destruct ((var_to_sym rel) ! dst) eqn:DST; simpl. { - destruct (in_or_not j (referenced_by s)). - { assert (dst <> i) by eauto with wellformed. - apply remove_from_sets_pass. - congruence. - rewrite PTree.gro by congruence. - apply Hrel; trivial. - } - rewrite remove_from_sets_notin by assumption. + assert (dst <> i) by eauto with wellformed. + apply remove_from_sets_pass. + congruence. rewrite PTree.gro by congruence. apply Hrel; trivial. } |