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.
---
 engine/evd.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index bbdb63a467..c6c4a71b22 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -247,9 +247,9 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 val existential_opt_value0 : evar_map -> existential -> constr option
 
 val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
-  'a array -> (Id.t * 'a) list
+  'a list -> (Id.t * 'a) list
 
-val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
+val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr
 
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
   evar_map ->  evar_map -> evar_map
-- 
cgit v1.2.3