# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223431125 14400
# Node ID b78a55b30f4ae9d58d96bd82b1c382f3ab6630bc
# Parent  7804f9d5249f90c02227261e3ac34e4c1dfd804a
Move [present] section earlier

diff -r 7804f9d5249f -r b78a55b30f4a src/MoreDep.v
--- a/src/MoreDep.v	Tue Oct 07 21:49:35 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 21:58:45 2008 -0400
@@ -398,6 +398,22 @@
 Inductive rtree : nat -> Set :=
 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
 
+Section present.
+  Variable x : nat.
+
+  Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
+    match t with
+      | Leaf => False
+      | RedNode _ a y b => present a \/ x = y \/ present b
+      | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
+    end.
+
+  Definition rpresent n (t : rtree n) : Prop :=
+    match t with
+      | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
+    end.
+End present.
+
 Notation "{< x >}" := (existT _ _ x).
 
 Definition balance1 n (a : rtree n) (data : nat) c2 :=
@@ -426,22 +442,6 @@
       end t2
   end.
 
-Section present.
-  Variable x : nat.
-
-  Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
-    match t with
-      | Leaf => False
-      | RedNode _ a y b => present a \/ x = y \/ present b
-      | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
-    end.
-
-  Definition rpresent n (t : rtree n) : Prop :=
-    match t with
-      | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
-    end.
-End present.
-
 Section insert.
   Variable x : nat.