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

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0a1b731e6b..3fb80432ad 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -99,7 +99,7 @@ val refresh_universes :
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env ->  evar_map ->
-  bool option -> Evar.t -> constr array -> constr array -> evar_map
+  bool option -> Evar.t -> constr list -> constr list -> evar_map
 
 val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
@@ -128,7 +128,7 @@ val check_evar_instance : unifier -> unify_flags ->
   env -> evar_map -> Evar.t -> constr -> evar_map
 
 val remove_instance_local_defs :
-  evar_map -> Evar.t -> 'a array -> 'a list
+  evar_map -> Evar.t -> 'a list -> 'a list
 
 val get_type_of_refresh :
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
-- 
cgit v1.2.3