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. *)