--- a/src/Match.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Match.v	Fri Nov 06 12:15:05 2009 -0500
@@ -89,6 +89,8 @@
       | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X))
     end.
 
+    ]]
+
    [[
 User error: Bound head variable
    ]]
@@ -450,6 +452,8 @@
 
     completer'.
 
+    ]]
+
     Coq loops forever at this point.  What went wrong? *)
   Abort.
 (* end thide *)
@@ -475,6 +479,8 @@
     | [ |- forall x, ?P ] => trivial
   end.
 
+  ]]
+
     [[
 User error: No matching clauses for match goal
     ]] *)
@@ -503,6 +509,8 @@
     | _ :: ls' => S (length ls')
   end.
 
+  ]]
+
    [[
 Error: The reference ls' was not found in the current environment
    ]]
@@ -516,6 +524,8 @@
     | _ :: ?ls' => S (length ls')
   end.
 
+  ]]
+
 [[
 Error: The reference S was not found in the current environment
 ]]