diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-08 16:25:10 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-08 16:25:10 +0100 |
| commit | a72250529e0bdb7ef10283cfdc230b7978fd999d (patch) | |
| tree | 2fac0af2af4f17ab83855e9ab1cd25aafc6e3c76 | |
| parent | cc1480ca6a68b2bb6db1bf5e292da07f47d6705e (diff) | |
| download | compcert-kvx-a72250529e0bdb7ef10283cfdc230b7978fd999d.tar.gz compcert-kvx-a72250529e0bdb7ef10283cfdc230b7978fd999d.zip | |
Proved non_empty_bblock_refl (was Admitted)
| -rw-r--r-- | mppa_k1c/Asmblock.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9da85fd0..6235589c 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -405,10 +405,10 @@ Lemma non_empty_bblock_refl: non_empty_bblock body exit -> Is_true (non_empty_bblockb body exit). Proof. -(* intros. destruct body; destruct exit. - all: unfold non_empty_bblock; try (left; discriminate); try (right; discriminate). - simpl in H. inv H. *) -Admitted. + intros. destruct body; destruct exit. + all: simpl; auto. + inv H; contradiction. +Qed. (* Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. |