Mercurial > cpdt > repo
changeset 545:4f6e7bab0d45
Make a theorem name more consistent
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Mar 2016 11:50:53 -0500 |
| parents | 71b85aaae868 |
| children | 306539f29eea |
| files | src/Match.v |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Match.v Thu Oct 15 07:42:00 2015 -0400 +++ b/src/Match.v Tue Mar 08 11:50:53 2016 -0500 @@ -985,7 +985,7 @@ -> P v2 u2 -> P (f v1 v2) (g u1 u2). - Theorem t6 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2). + Theorem t7 : forall v1 v2, Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2). (** We can prove the goal by calling [insterKeep] with a tactic that tries to find and apply a [Q] hypothesis over a variable about which we do not yet know any [P] facts. We need to begin this tactic code with [idtac; ] to get around a strange limitation in Coq's proof engine, where a first-class tactic argument may not begin with a [match]. *)