--- a/src/Reflection.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/Reflection.v	Fri Nov 06 12:15:05 2009 -0500
@@ -118,6 +118,8 @@
 
   prove_even_reflective.
 
+  ]]
+
   [[
 
 User error: No matching clauses for match goal
@@ -129,6 +131,8 @@
 
   exact (partialOut (check_even 255)).
 
+  ]]
+
   [[
 
   Error: The term "partialOut (check_even 255)" has type
@@ -633,12 +637,19 @@
   Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1
     -> z + (8 # 1) * x == 20 # 1
     -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1.
+
+    ]]
+
 [[
 
     intros; reflectContext; assumption.
+
+    ]]
 [[
   Qed.
 
+]]
+
   Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function.  These hints outline a particular possible solution.  Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==].
 
 %\begin{enumerate}%#<ol>#
@@ -680,6 +691,8 @@
                   end ]
       end.
 
+]]
+
 #</ol>#%\end{enumerate}%
 #</li>#