diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-05 12:07:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-05 12:07:26 +0200 |
commit | 684fd1a0989e6daa3bc20ddba925481a4f2182bf (patch) | |
tree | 1c6275fd1c4b8af029561aa362034078b8c2cbba /backend/NeedDomain.v | |
parent | be6875023bc0b33701042cdf923cd9e07b4fb316 (diff) | |
parent | e9fa9cbdc761f8c033e9b702f7485982faed3f7d (diff) | |
download | compcert-684fd1a0989e6daa3bc20ddba925481a4f2182bf.tar.gz compcert-684fd1a0989e6daa3bc20ddba925481a4f2182bf.zip |
Merge branch 'master' into json_export
Diffstat (limited to 'backend/NeedDomain.v')
-rw-r--r-- | backend/NeedDomain.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 8beff265..770648b1 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -840,7 +840,7 @@ Lemma default_needs_of_condition_sound: eval_condition cond args2 m2 = Some b. Proof. intros. apply eval_condition_inj with (f := inject_id) (m1 := m1) (vl1 := args1); auto. - apply val_list_inject_lessdef. apply lessdef_vagree_list. auto. + apply val_inject_list_lessdef. apply lessdef_vagree_list. auto. Qed. Lemma default_needs_of_operation_sound: @@ -866,7 +866,7 @@ Proof. eassumption. auto. auto. auto. instantiate (1 := op). intros. apply val_inject_lessdef; auto. apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto. - apply val_list_inject_lessdef; eauto. + apply val_inject_list_lessdef; eauto. eauto. intros (v2 & A & B). exists v2; split; auto. apply vagree_lessdef. apply val_inject_lessdef. auto. |