# HG changeset patch # User Adam Chlipala # Date 1295282529 18000 # Node ID f4768d5a75ebd47502ee7829a2d4232ac948da15 # Parent 25ec92be5ad2607afe02453c0cf24dbb5cf3aa5a Typo fix diff -r 25ec92be5ad2 -r f4768d5a75eb src/Match.v --- a/src/Match.v Fri Jan 14 15:43:32 2011 -0500 +++ b/src/Match.v Mon Jan 17 11:42:09 2011 -0500 @@ -544,7 +544,7 @@ ]] - We use the [pose] tactic, which extends the proof context with a new variable that is set equal to particular a term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context. + We use the [pose] tactic, which extends the proof context with a new variable that is set equal to a particular term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context. [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *)