Finished vertical spacing

src/Large.v

@@ -193,7 +193,6 @@ Theorem eval_times : forall k e,
 Error: Expects a disjunctive pattern with 3 branches.
 >>
   *)
-
 Abort.
 
 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases.  To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place.  Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *)
@@ -562,8 +561,7 @@ Finished transaction in 0. secs (0.068004u,0.s)
     (** <<
 Finished transaction in 2. secs (1.264079u,0.s)
       >>
-
-      Why has the search time gone up so much?  The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *)
+      %\vspace{-.15in}%Why has the search time gone up so much?  The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *)
 
 (* begin thide *)
     Restart.

src/LogicProg.v

@@ -946,7 +946,6 @@ Section autorewrite.
     Lemma f_f_f' : forall x, f (f (f x)) = f x.
       intros; autorewrite with core.
       (** [[
-
   ============================
    g (g (g x)) = g x
 

src/Match.v

@@ -267,12 +267,10 @@ Section firstorder'.
 
   Theorem fo' : forall x, P x -> S x.
 (* begin thide *)
-    (** [[
+    (** %\vspace{-.25in}%[[
     completer'.
- 
     ]]
-
-    Coq loops forever at this point.  What went wrong? *)
+    %\vspace{-.15in}%Coq loops forever at this point.  What went wrong? *)
 
   Abort.
 (* end thide *)
@@ -292,7 +290,7 @@ Qed.
 
 (* begin thide *)
 Theorem t1' : forall x : nat, x = x.
-(** [[
+(** %\vspace{-.25in}%[[
   match goal with
     | [ |- forall x, ?P ] => trivial
   end.
@@ -320,7 +318,6 @@ Abort.
 (** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor.  However, there are a few syntactic conventions involved in getting programs to be accepted.  The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs.
 
    To illustrate, let us try to write a simple list length function.  We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac].
-
    [[
 Ltac length ls :=
   match ls with
@@ -334,7 +331,6 @@ Error: The reference ls' was not found in the current environment
 >>
 
    At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac.
-
    [[
 Ltac length ls :=
   match ls with
@@ -356,7 +352,7 @@ Ltac length ls :=
     | _ :: ?ls' => constr:(S (length ls'))
   end.
 
-(** This definition is accepted.  It can be a little awkward to test Ltac definitions like this.  Here is one method. *)
+(** This definition is accepted.  It can be a little awkward to test Ltac definitions like this one.  Here is one method. *)
 
 Goal False.
   let n := length (1 :: 2 :: 3 :: nil) in
@@ -365,7 +361,6 @@ Goal False.
   n := S (length (2 :: 3 :: nil)) : nat
   ============================
    False
- 
    ]]
 
    We use the %\index{tactics!pose}%[pose] tactic, which extends the proof context with a new variable that is set equal to a particular term.  We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context.
@@ -889,7 +884,7 @@ Section t7.
 No more subgoals but non-instantiated existential variables :
 Existential 1 =
 >>
-       [[
+       %\vspace{-.35in}%[[
 ?4384 : [A : Type
          B : Type
          Q : A -> Prop
@@ -904,7 +899,6 @@ Existential 1 =
          H : Q v1
          H0 : Q v2
          H' : Q v2 -> exists u : B, P v2 u |- Q v2] 
- 
          ]]
 
          There is another similar line about a different existential variable.  Here, "existential variable" means what we have also called "unification variable."  In the course of the proof, some unification variable [?4384] was introduced but never unified.  Unification variables are just a device to structure proof search; the language of Gallina proof terms does not include them.  Thus, we cannot produce a proof term without instantiating the variable.

src/Reflection.v

@@ -44,7 +44,6 @@ Even_SS
   (Even_SS
      (Even_SS
         (Even_SS
- 
     ]]
 
     %\noindent%...and so on.  This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even.  The final proof term has length super-linear in the input value.  Coq's implicit arguments mechanism is hiding the values given for parameter [n] of [Even_SS], which is why the proof term only appears linear here.  Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent.  Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough.
@@ -66,7 +65,6 @@ Definition paartial := partial.
 Print partial.
 (** %\vspace{-.15in}% [[
 Inductive partial (P : Prop) : Set :=  Proved : P -> [P] | Uncertain : [P]
- 
     ]]
 
     A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
@@ -174,7 +172,6 @@ true_galore =
 fun H : True /\ True =>
 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
      : True /\ True -> True \/ True /\ (True -> True)
- 
     ]]
 
     As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules.  For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
@@ -240,7 +237,6 @@ Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
 Qed.
 
 Print true_galore'.
-
 (** %\vspace{-.15in}% [[
 true_galore' = 
 tautTrue

staging/updates.rss

@@ -11,6 +11,14 @@
 <webMaster>adam@chlipala.net</webMaster>
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
+<item>
+        <title>Vertical spacing</title>
+        <pubDate>Wed, 1 Aug 2012 17:29:20 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>This is a mundane revision where I've normalized the vertical space separators between text sections.  Like the last release, this one won't build for LaTeX without a coqdoc patch that may not be in Coq's Subversion repos yet.  This is the home stretch; I am going to make a proofreading pass through everything, and then I'll be looking for other proofreaders to help come up with the final version to be published by MIT Press!</description>
+</item>
+
 <item>
         <title>Taking advantage of coqdoc changes</title>
         <pubDate>Fri, 27 Jul 2012 16:48:35 EDT</pubDate>