From ecbecdd399d0d685ffed2024e864dc4aaccdfbf6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 11:48:04 +0100 Subject: Extended arguments to annotations, continued: - Simplifications in RTLgen. - Updated Cexec. --- common/Events.v | 34 ---------------------------------- common/Values.v | 6 ++++++ 2 files changed, 6 insertions(+), 34 deletions(-) (limited to 'common') 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: -- cgit