From db8ffccb25f763d193a63dbe65ff079619a3780e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Jun 2014 02:10:44 +0200
Subject: Small short optimization of instantiation in Evd.

---
 pretyping/evd.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 09e34c6aa4..902ec9f154 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -242,7 +242,8 @@ let make_evar_instance_array info args =
   | true :: filter, (id, _, _) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      (id, c) :: instrec filter ctxt (succ i)
+      if isVarId id c then instrec filter ctxt (succ i)
+      else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
-- 
cgit v1.2.3