Mercurial > cpdt > repo

diff src/MoreDep.v @ 294:1b6c81e51799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes added while proofreading JFR camera-ready
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 13:44:57 -0500
parents 2c88fc1dbe33
children 559ec7328410
line wrap: on
line diff
--- a/src/MoreDep.v	Wed Nov 10 16:34:46 2010 -0500
+++ b/src/MoreDep.v	Thu Dec 09 13:44:57 2010 -0500
@@ -665,7 +665,7 @@
 
     (** The balance correctness theorems are simple first-order logic equivalences, where we use the function [projT2] to project the payload of a [sigT] value. *)
 
-    Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
+    Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
       present z (projT2 (balance1 a y b))
       <-> rpresent z a \/ z = y \/ present z b.
       destruct a; present_balance.