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 | |
parent | 4622f49fd089ae47d0c853343cb0a05f986c962a (diff) | |
download | compcert-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.tar.gz compcert-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.zip |
Extended arguments to annotations, continued:
- Simplifications in RTLgen.
- Updated Cexec.
Diffstat (limited to 'common')
-rw-r--r-- | common/Events.v | 34 | ||||
-rw-r--r-- | common/Values.v | 6 |
2 files changed, 6 insertions, 34 deletions
diff --git a/common/Events.v b/common/Events.v index ad59ece9..15bf4e12 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1915,37 +1915,3 @@ Qed. End EVAL_ANNOT_ARG_LESSDEF. -(** Extensionality *) - -Section EVAL_ANNOT_ARG_EXTEN. - -Variable A: Type. -Variable ge: Senv.t. -Variables e1 e2: A -> val. -Variable sp: val. -Variable m: mem. - -Lemma eval_annot_arg_exten: - forall a v, eval_annot_arg ge e1 sp m a v -> - (forall x, In x (params_of_annot_arg a) -> e2 x = e1 x) -> - eval_annot_arg ge e2 sp m a v. -Proof. - induction 1; simpl; intros EXT; try (now constructor). -- rewrite <- EXT by auto. constructor. -- constructor; eauto using in_or_app. -Qed. - -Lemma eval_annot_args_exten: - forall a v, eval_annot_args ge e1 sp m a v -> - (forall x, In x (params_of_annot_args a) -> e2 x = e1 x) -> - eval_annot_args ge e2 sp m a v. -Proof. - induction 1; simpl; intros EXT; constructor. - eapply eval_annot_arg_exten; eauto using in_or_app. - eapply IHlist_forall2; eauto using in_or_app. -Qed. - -End EVAL_ANNOT_ARG_EXTEN. - - - 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: |