From e69aad0acf0ae1892ff62dc639389a7c88e66772 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 8 Nov 2013 02:11:57 +0100
Subject: Useless Array.of_list

---
 proofs/goal.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index c660f403f..c40570c2c 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -535,8 +535,8 @@ module V82 = struct
     in
     let evi = Typeclasses.mark_unresolvable evi in
     let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
-    let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in
-    let inst = Array.of_list (List.map mkVar ids) in
+    let ctxt = Environ.named_context_of_val hyps in
+    let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (build evk, ev, evars)
 
-- 
cgit v1.2.3