# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225046361 14400
# Node ID d6b1e9de7fc1e8059aa20acc230ea48cb9cd299b
# Parent  091583baf3459be5f7ac80e01cbfd11c60912f82
Free variables in unification variables issue

diff -r 091583baf345 -r d6b1e9de7fc1 src/Match.v
--- a/src/Match.v	Sun Oct 26 14:11:41 2008 -0400
+++ b/src/Match.v	Sun Oct 26 14:39:21 2008 -0400
@@ -412,3 +412,31 @@
     Coq loops forever at this point.  What went wrong? *)
   Abort.
 End firstorder'.
+
+(** A few examples should illustrate the issue.  Here we see a [match]-based proof that works fine: *)
+
+Theorem t1 : forall x : nat, x = x.
+  match goal with
+    | [ |- forall x, _ ] => trivial
+  end.
+Qed.
+
+(** This one fails. *)
+
+Theorem t1' : forall x : nat, x = x.
+(** [[
+
+  match goal with
+    | [ |- forall x, ?P ] => trivial
+  end.
+
+    [[
+User error: No matching clauses for match goal
+    ]] *)
+Abort.
+
+(** The problem is that unification variables may not contain locally-bound variables.  In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x].  By using a wildcard in the earlier version, we avoided this restriction.
+
+   The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables.  That unification variable is then bound to a function from the free variables to the "real" value.  In Coq 8.1 and earlier, there is no such workaround.
+
+   No matter which version you use, it is important to be aware of this restriction.  As we have alluded to, the restriction is the culprit behind the infinite-looping behavior of [completer'].  We unintentionally match quantified facts with the modus ponens rule, circumventing the "already present" check and leading to different behavior. *)