diff options
Diffstat (limited to 'backend/CSEdomain.v')
-rw-r--r-- | backend/CSEdomain.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index 9641d012..3fee2db6 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -149,7 +149,7 @@ Proof. - split; simpl; intros. + contradiction. + rewrite PTree.gempty in H; discriminate. - + rewrite PMap.gi in H; contradiction. + + contradiction. - contradiction. - rewrite PTree.gempty in H; discriminate. Qed. |