# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1224697232 14400
# Node ID 6bf40eff5e98fc77795995d1a72c8aaf03a9fd59
# Parent  464db50b210a99dd403d1574c44711dd3bc9968d
call-by-name is really call-by-need

diff -r 464db50b210a -r 6bf40eff5e98 src/Equality.v
--- a/src/Equality.v	Wed Oct 22 09:43:37 2008 -0400
+++ b/src/Equality.v	Wed Oct 22 13:40:32 2008 -0400
@@ -37,7 +37,7 @@
 (* begin thide *)
   (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters.  Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
 
-     The delta rule is for unfolding global definitions.  We can use it here to unfold the definition of [pred'].  We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules.  There is an analogous tactic [lazy] for call-by-name reduction. *)
+     The delta rule is for unfolding global definitions.  We can use it here to unfold the definition of [pred'].  We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules.  There is an analogous tactic [lazy] for call-by-need reduction. *)
 
   cbv delta.
   (** [[