From 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Sep 2018 18:55:30 +0200
Subject: Use lists instead of arrays in evar instances.

This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
---
 kernel/inferCumulativity.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/inferCumulativity.ml')

diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index f987164d52..662ad550b8 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     end
   | FEvar ((_,args),e) ->
     let variances = infer_stack infos variances stk in
-    infer_vect infos variances (Array.map (mk_clos e) args)
+    infer_list infos variances (List.map (mk_clos e) args)
   | FRel _ -> infer_stack infos variances stk
   | FInt _ -> infer_stack infos variances stk
   | FFloat _ -> infer_stack infos variances stk
@@ -168,6 +168,9 @@ and infer_stack infos variances (stk:CClosure.stack) =
 and infer_vect infos variances v =
   Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
 
+and infer_list infos variances v =
+  List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
 let infer_term cv_pb env variances c =
   let open CClosure in
   let infos = (create_clos_infos all env, create_tab ()) in
-- 
cgit v1.2.3