diff options
Diffstat (limited to 'backend/Inliningspec.v')
| -rw-r--r-- | backend/Inliningspec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 331f8b06..dfd96333 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -52,9 +52,9 @@ Proof. P dm fenv -> P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) (fold_left add_globdef l fenv)). - { induction l; simpl; intros. + { induction l; simpl; intros. - auto. - - apply IHl. apply ADD; auto. + - apply IHl. apply ADD; auto. } intros. apply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. @@ -63,8 +63,8 @@ Lemma fenv_compat_linkorder: forall cunit prog fenv, linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv. Proof. - intros; red; intros. apply H0 in H1. - destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). + intros; red; intros. apply H0 in H1. + destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). inv Q. inv H3. auto. Qed. @@ -702,7 +702,7 @@ Lemma tr_function_linkorder: tr_function cunit f f' -> tr_function prog f f'. Proof. - intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. + intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. Qed. Lemma transf_function_spec: |