From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 19 Aug 2011 09:13:09 +0000 Subject: Cleaned up old commented-out parts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Determinism.v | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'common/Determinism.v') 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 -> -- cgit