diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 11:48:04 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 11:48:04 +0100 |
| commit | ecbecdd399d0d685ffed2024e864dc4aaccdfbf6 (patch) | |
| tree | 5546d9139c4c1586355f9c6b8e43cc8b1c812042 /common/Values.v | |
| parent | 4622f49fd089ae47d0c853343cb0a05f986c962a (diff) | |
| download | compcert-kvx-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.tar.gz compcert-kvx-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.zip | |
Extended arguments to annotations, continued:
- Simplifications in RTLgen.
- Updated Cexec.
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index a12fb636..984da4ed 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1381,6 +1381,12 @@ Proof. left; congruence. tauto. tauto. Qed. +Lemma lessdef_list_trans: + forall vl1 vl2, lessdef_list vl1 vl2 -> forall vl3, lessdef_list vl2 vl3 -> lessdef_list vl1 vl3. +Proof. + induction 1; intros vl3 LD; inv LD; constructor; eauto using lessdef_trans. +Qed. + (** Compatibility of operations with the [lessdef] relation. *) Lemma load_result_lessdef: |