diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-30 19:26:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-30 19:26:11 +0200 |
| commit | e9fa9cbdc761f8c033e9b702f7485982faed3f7d (patch) | |
| tree | 07eef17ccca466fd39d8d3ab0aab821ebfce177f /backend/NeedDomain.v | |
| parent | 7dd10e861c7ecbe74a781a6050ae1341bbe45dcd (diff) | |
| download | compcert-kvx-e9fa9cbdc761f8c033e9b702f7485982faed3f7d.tar.gz compcert-kvx-e9fa9cbdc761f8c033e9b702f7485982faed3f7d.zip | |
Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Val.lessdef, etc.
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. |