diff src/Coinductive.v @ 442:89c67796754e

Undo some overzealous vspace tweaks
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 16:09:37 -0400
parents f923024bd284
children f28bdd8414e0
line wrap: on
line diff
--- a/src/Coinductive.v	Wed Aug 01 15:52:50 2012 -0400
+++ b/src/Coinductive.v	Wed Aug 01 16:09:37 2012 -0400
@@ -29,7 +29,7 @@
 Fixpoint bad (u : unit) : P := bad u.
 ]]
 
-%\smallskip{}%This would leave us with [bad tt] as a proof of [P].
+This would leave us with [bad tt] as a proof of [P].
 
 There are also algorithmic considerations that make universal termination very desirable.  We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules.  Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps.  It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.