Mercurial > cpdt > repo
changeset 301:f4768d5a75eb
Typo fix
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 17 Jan 2011 11:42:09 -0500 |
| parents | 25ec92be5ad2 |
| children | 7b38729be069 |
| files | src/Match.v |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- 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. *)