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/evarutil.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 1dec63aaf0..b5c7ccb283 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -88,7 +88,7 @@ val new_evar_instance : named_context_val -> evar_map -> types -> constr list -> evar_map * constr -val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list +val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option -- cgit v1.2.3