diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-10 12:13:12 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-10 12:13:12 +0000 |
| commit | 02779dbc71c0f6985427c47ec05dd25b44dd859c (patch) | |
| tree | cdff116e8c7e5d82ae6943428018f39d1ce81d60 /backend/Stackingproof.v | |
| parent | e29b0c71f446ea6267711c7cc19294fd93fb81ad (diff) | |
Glasnost: making transparent a number of definitions that were opaque
for no good reason.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 4ce8c25..d97ec93 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -779,9 +779,6 @@ Lemma agree_frame_set_reg: Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. - rewrite Locmap.gso; auto. red; auto. - rewrite Locmap.gso; auto. red; auto. - rewrite Locmap.gso; auto. red; auto. apply wt_setloc; auto. Qed. @@ -857,8 +854,6 @@ Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. constructor; auto; intros. -(* unused *) - rewrite Locmap.gso; auto. red; auto. (* local *) unfold Locmap.set. simpl. destruct (Loc.eq (S (Local ofs ty)) (S (Local ofs0 ty0))). inv e. eapply gss_index_contains_inj; eauto. @@ -867,8 +862,6 @@ Proof. (* outgoing *) rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. simpl; auto. red; auto. -(* incoming *) - rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto. red; auto. (* retaddr *) @@ -899,8 +892,6 @@ Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. constructor; auto; intros. -(* unused *) - rewrite Locmap.gso; auto. red; auto. (* local *) rewrite Locmap.gso. eapply gso_index_contains_inj; eauto. simpl; auto. red; auto. (* outgoing *) @@ -911,8 +902,6 @@ Proof. red; intros. eapply Mem.perm_store_1; eauto. eapply gso_index_contains_inj; eauto. red. eapply Loc.overlap_aux_false_1; eauto. -(* incoming *) - rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto with stacking. red; auto. (* retaddr *) |