From 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 13 Jan 2010 09:53:07 +0000
Subject: Backtracking on commit 1220

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/OrderedOption.v | 96 -------------------------------------------------
 1 file changed, 96 deletions(-)
 delete mode 100755 backend/OrderedOption.v

(limited to 'backend/OrderedOption.v')

diff --git a/backend/OrderedOption.v b/backend/OrderedOption.v
deleted file mode 100755
index b2cebe2..0000000
--- a/backend/OrderedOption.v
+++ /dev/null
@@ -1,96 +0,0 @@
-Require Import FSets.
-
-(* Definition of options types as ordered types,
-    in order to define weights *)
-
-Module OrderedOpt (O : OrderedType) <: OrderedType.
-
-Definition t := option O.t.
-
-Inductive eq_ : t -> t -> Prop :=
-|None_eq : eq_ None None
-|Some_eq : forall x y, O.eq x y -> eq_ (Some x) (Some y).
-
-Definition eq := eq_.
-
-Inductive lt_ : t -> t -> Prop := 
-|None_lt : forall o : O.t, lt_ None (Some o)
-|Some_lt : forall o o', O.lt o o' -> lt_ (Some o) (Some o').
-
-Definition lt := lt_.
-
-Lemma eq_refl : forall x : t, eq x x.
-
-Proof.
-unfold eq;intro x;destruct x;constructor;apply O.eq_refl.
-Qed.
-
-Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-
-Proof.
-unfold eq;intros x y H;destruct x;destruct y.
-constructor;inversion H;apply O.eq_sym;assumption.
-inversion H.
-inversion H.
-assumption.
-Qed.
-
-Lemma eq_trans : forall x y z, eq x y -> eq y z -> eq x z.
-
-Proof.
-unfold eq;intros x y z H H0.
-inversion H;inversion H0.
-constructor.
-rewrite <-H2 in H4;inversion H4.
-rewrite <-H3 in H4;inversion H4.
-rewrite <-H3 in H5;inversion H5;subst.
-constructor;apply (O.eq_trans H1 H4).
-Qed.
-
-Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z.
-
-Proof.
-unfold lt;intros x y z H H0.
-inversion H;inversion H0;constructor.
-rewrite <-H3 in H4;inversion H4.
-rewrite <-H3 in H5;inversion H5.
-subst.
-apply (O.lt_trans H1 H4).
-Qed.
-
-Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
-
-Proof.
-intros x y H.
-unfold eq;intro Heq.
-inversion H;inversion Heq.
-rewrite <-H3 in H1;inversion H1.
-rewrite <-H0 in H3;inversion H3.
-rewrite <-H1 in H3;inversion H3.
-subst;inversion H4;inversion H5;subst.
-elim (O.lt_not_eq H0 H3).
-Qed.
-
-Lemma compare : forall x y : t, Compare lt eq x y.
-
-Proof.
-intros x y.
-destruct x;destruct y.
-destruct (O.compare t0 t1);
-[apply LT;unfold lt|apply EQ;unfold eq|apply GT;unfold lt];constructor;assumption.
-apply GT;unfold lt;constructor.
-apply LT;unfold lt;constructor.
-apply EQ;unfold eq;constructor.
-Qed.
-
-Lemma eq_dec : forall x y, {eq x y}+{~eq x y}.
-
-Proof.
-intros x y.
-destruct (compare x y).
-right. apply lt_not_eq. assumption.
-left. assumption.
-right. intro H. generalize (eq_sym _ _ H). intro H0. elim (lt_not_eq _ _ l H0).
-Qed.
-
-End OrderedOpt.
\ No newline at end of file
-- 
cgit v1.2.3