diff options
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 90f03c1c..fc765ce5 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -54,11 +54,11 @@ Proof. intros until r0. repeat rewrite PTree.gsspec. destruct (peq id1 name); destruct (peq id2 name). congruence. - intros. inv H. elimtype False. + intros. inv H. exfalso. apply valid_fresh_absurd with r0 s1. apply H1. left; exists id2; auto. eauto with rtlg. - intros. inv H2. elimtype False. + intros. inv H2. exfalso. apply valid_fresh_absurd with r0 s1. apply H1. left; exists id1; auto. eauto with rtlg. |