From 88f8f535084567d5d52d510802b3cee15c2b3503 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 29 Nov 2019 15:38:20 +0100
Subject: Optimization: take advantage that we don't use arrays anymore in
 substitutions.

---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 85e24f87b7..802a32b0e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -198,7 +198,7 @@ let type_of_apply env func funt argsv argstv =
         let argt = argstv.(i) in
         let c1 = term_of_fconstr c1 in
         begin match conv_leq false env argt c1 with
-        | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+        | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2)
         | exception NotConvertible ->
           error_cant_apply_bad_type env
             (i+1,c1,argt)
-- 
cgit v1.2.3