# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1319554560 14400
# Node ID de7db21a016c0e79715b7c9f6c362877f71f9ace
# Parent  f3154417cd41cb384905eee2516e35b14432fb43
Fix template

diff -r f3154417cd41 -r de7db21a016c src/Coinductive.v
--- 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.