# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1457455853 18000
# Node ID 4f6e7bab0d4527018956bc2897c1f878726ca162
# Parent  71b85aaae8682a475bbc05c2f411110ff3018aef
Make a theorem name more consistent

diff -r 71b85aaae868 -r 4f6e7bab0d45 src/Match.v
--- 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]. *)