diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:28:21 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:28:21 +0100 |
| commit | 27b985393cd8d90a3d6f5e9f13bdf90e4300bb8e (patch) | |
| tree | 69a0f2976b0f195d4877ec7d8749a7d4d968345f /backend/CSE2proof.v | |
| parent | bc89c7487901c6056c84bf598ea4ab6535de68c2 (diff) | |
| download | compcert-kvx-27b985393cd8d90a3d6f5e9f13bdf90e4300bb8e.tar.gz compcert-kvx-27b985393cd8d90a3d6f5e9f13bdf90e4300bb8e.zip | |
rm useless admitted lemma
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 3799e38b..4d503f90 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -204,11 +204,6 @@ Proof. Qed. Local Hint Resolve kill_sym_val_referenced : wellformed. -Lemma in_or_not: - forall (x : reg) l, - (In x l) \/ ~(In x l). -Admitted. - Lemma remove_from_sets_notin: forall dst l sets j, not (In j l) -> |