From 8974b52f7bd2fd1c14fe326453a2be7490c3c392 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Oct 2014 17:16:49 -0700
Subject: [PATCH] perf(library/unifier): avoid unnecessary wasteful computation

---
 src/library/unifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 6ad4548f5b..cf9be2b0c6 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1440,7 +1440,7 @@ struct unifier_fn {
                 num++;
                 t = binding_body(t);
             }
-            if (num == margs.size())
+            if (num >= margs.size())
                 return mtype;
             return ensure_sufficient_args_core(mtype, 0, cs);
         }