Module PreservationStack

Load PreservationHeader.

Lemma goal : forall sf (Hin: In sf (State.stack s2)), stackframe_weak_inv prog s2 sf.

Proof.

destruct sf; intros; try exact I.
destruct inhpath; destruct k.
  Require Import PreservationStackKconstrotherBase.
  eauto using goal.
  Require Import PreservationStackKconstrotherField.
  destruct kind; eauto using goal.
Require Import PreservationStackKconstrothercells.
eauto using goal.
destruct inhpath; destruct k.
  Require Import PreservationStackKdestrotherBase.
  eauto using goal.
  Require Import PreservationStackKdestrotherField.
  destruct kind; eauto using goal.
Require Import PreservationStackKdestrcell.
eauto using goal.
Qed.

End Preservation.

Copyright 2009, 2010, 2011 Tahina Ramananandro. This HTML documentation generated by coq2html.mll (part of Compcert 1.7 by Xavier Leroy)