diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-19 09:13:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-19 09:13:09 +0000 |
| commit | 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 (patch) | |
| tree | e324aff1a958e0a5d83f805ff3ca1d9eb07939f4 /common/Determinism.v | |
| parent | 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e (diff) | |
| download | compcert-kvx-7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1.tar.gz compcert-kvx-7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1.zip | |
Cleaned up old commented-out parts
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Determinism.v')
| -rw-r--r-- | common/Determinism.v | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/common/Determinism.v b/common/Determinism.v index 29cc6958..778ba224 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -126,25 +126,6 @@ Proof. inv H4; inv H3. inv H7; inv H6. auto. Qed. -(* -Lemma possible_event_final_world: - forall w ev w1 w2, - possible_event w ev w1 -> possible_event w ev w2 -> w1 = w2. -Proof. - intros. inv H; inv H0; congruence. -Qed. - -Lemma possible_trace_final_world: - forall w0 t w1, possible_trace w0 t w1 -> - forall w2, possible_trace w0 t w2 -> w1 = w2. -Proof. - induction 1; intros. - inv H. auto. - inv H1. assert (w2 = w5) by (eapply possible_event_final_world; eauto). - subst; eauto. -Qed. -*) - CoInductive possible_traceinf: world -> traceinf -> Prop := | possible_traceinf_cons: forall w1 ev w2 T, possible_event w1 ev w2 -> |