--- a/src/Coinductive.v	Tue Oct 25 10:51:31 2011 -0400
+++ b/src/Coinductive.v	Tue Oct 25 10:56:00 2011 -0400
@@ -96,7 +96,7 @@
       ]]
 *)
 
-(* end thide *) 
+(* end thide *)
 
 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks.  However, there are important restrictions that are dual to the restrictions on the use of inductive types.  Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls.  Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.