Mercurial > cpdt > repo
diff src/Generic.v @ 360:e0d91bcf70ec
Pass through old content of Reflection
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 02 Nov 2011 14:48:25 -0400 |
parents | 059c51227e69 |
children | d1276004eec9 |
line wrap: on
line diff
--- a/src/Generic.v Tue Nov 01 12:34:00 2011 -0400 +++ b/src/Generic.v Wed Nov 02 14:48:25 2011 -0400 @@ -530,7 +530,7 @@ (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0". >> - Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the [pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *) + Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the %\index{tactics!pattern}%[pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *) pattern v. (** %\vspace{-.15in}%[[