aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml4
-rw-r--r--engine/evarutil.ml10
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml41
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/termops.ml8
-rw-r--r--engine/univSubst.ml2
7 files changed, 33 insertions, 38 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 4508633858..ca681e58f8 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -355,7 +355,7 @@ let iter_with_full_binders sigma g f n c =
| Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
- | Evar (_,l) -> Array.Fun1.iter f n l
+ | Evar (_,l) -> List.iter (fun c -> f n c) l
| Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
@@ -717,7 +717,7 @@ let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq
let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
let of_existential : Constr.existential -> existential =
- let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+ let gen : type a b. (a,b) eq -> 'c * b list -> 'c * a list = fun Refl x -> x in
gen unsafe_eq
let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fdcdfe11f4..5fcadfcef7 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -200,7 +200,7 @@ let make_pure_subst evi args =
match args with
| a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
| _ -> anomaly (Pp.str "Instance does not match its signature."))
- (evar_filtered_context evi) (Array.rev_to_list args,[]))
+ (evar_filtered_context evi) (List.rev args,[]))
(*------------------------------------*
* functional operations on evar sets *
@@ -448,7 +448,7 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
- evd, mkEvar (newevk,Array.of_list instance)
+ evd, mkEvar (newevk, instance)
let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
@@ -506,7 +506,7 @@ let generalize_evar_over_rels sigma (ev,args) =
List.fold_left2
(fun (c,inst as x) a d ->
if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
- (evi.evar_concl,[]) (Array.to_list args) sign
+ (evi.evar_concl,[]) args sign
(************************************)
(* Removing a dependency in an evar *)
@@ -594,7 +594,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
(* No dependency at all, we can keep this ev's context hyp *)
(ri, true::filter)
with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
- ctxt (Array.to_list l) (Id.Map.empty,[]) in
+ ctxt l (Id.Map.empty,[]) in
(* Check if some rid to clear in the context of ev has dependencies
in the type of ev and adjust the source of the dependency *)
let _nconcl =
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
match EConstr.kind evd c with
| Evar (n, l) ->
let acc = Evar.Set.add n acc in
- Array.fold_left evrec acc l
+ List.fold_left evrec acc l
| _ -> EConstr.fold evd evrec acc c
in
evrec Evar.Set.empty t
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
diff --git a/engine/evd.ml b/engine/evd.ml
index 65fe261ff4..5642145f6d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -233,32 +233,27 @@ exception NotInstantiatedEvar
(* Note: let-in contributes to the instance *)
let evar_instance_array test_id info args =
- let len = Array.length args in
- let rec instrec filter ctxt i = match filter, ctxt with
- | [], [] ->
- if Int.equal i len then []
- else instance_mismatch ()
- | false :: filter, _ :: ctxt ->
- instrec filter ctxt i
- | true :: filter, d :: ctxt ->
- if i < len then
- let c = Array.unsafe_get args i in
- if test_id d c then instrec filter ctxt (succ i)
- else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
- else instance_mismatch ()
+ let rec instrec filter ctxt args = match filter, ctxt, args with
+ | [], [], [] -> []
+ | false :: filter, _ :: ctxt, args ->
+ instrec filter ctxt args
+ | true :: filter, d :: ctxt, c :: args ->
+ if test_id d c then instrec filter ctxt args
+ else (NamedDecl.get_id d, c) :: instrec filter ctxt args
| _ -> instance_mismatch ()
in
match Filter.repr (evar_filter info) with
| None ->
- let map i d =
- if (i < len) then
- let c = Array.unsafe_get args i in
- if test_id d c then None else Some (NamedDecl.get_id d, c)
- else instance_mismatch ()
+ let rec instance ctxt args = match ctxt, args with
+ | [], [] -> []
+ | d :: ctxt, c :: args ->
+ if test_id d c then instance ctxt args
+ else (NamedDecl.get_id d, c) :: instance ctxt args
+ | _ -> instance_mismatch ()
in
- List.map_filter_i map (evar_context info)
+ instance (evar_context info) args
| Some filter ->
- instrec filter (evar_context info) 0
+ instrec filter (evar_context info) args
let make_evar_instance_array info args =
evar_instance_array (NamedDecl.get_id %> isVarId) info args
@@ -794,7 +789,7 @@ let restrict evk filter ?candidates ?src evd =
| _ -> Evar.Set.add evk evd.last_mods in
let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
let ctxt = Filter.filter_list filter (evar_context evar_info) in
- let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
+ let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
let body = mkEvar(evk',id_inst) in
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
@@ -1405,7 +1400,7 @@ let evars_of_term evd c =
let rec evrec acc c =
let c = MiniEConstr.whd_evar evd c in
match kind c with
- | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
| _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
@@ -1413,7 +1408,7 @@ let evars_of_term evd c =
let evar_nodes_of_term c =
let rec evrec acc c =
match kind c with
- | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | Evar (n, l) -> Evar.Set.add n (List.fold_left evrec acc l)
| _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
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
diff --git a/engine/termops.ml b/engine/termops.ml
index 16f2a87c1e..6d779e6a35 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c =
if b' == b then c
else mkProj (p, b')
| Evar (e,al) ->
- let al' = Array.map_left (f l) al in
- if Array.for_all2 (==) al' al then c
+ let al' = List.map_left (f l) al in
+ if List.for_all2 (==) al' al then c
else mkEvar (e, al')
| Case (ci,p,b,bl) ->
(* In v8 concrete syntax, predicate is after the term to match! *)
@@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
let c' = f l c in
if c' == c then cstr else mkProj (p, c')
| Evar (e,al) ->
- let al' = Array.map (f l) al in
- if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+ let al' = List.map (f l) al in
+ if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
| Case (ci,p,c,bl) when userview ->
let p' = map_return_predicate_with_full_binders sigma g f l ci p in
let c' = f l c in
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 6000650ad9..a691239ee2 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,7 +131,7 @@ let nf_evars_and_universes_opt_subst f subst =
let rec aux c =
match kind c with
| Evar (evk, args) ->
- let args = Array.map aux args in
+ let args = List.map aux args in
(match try f (evk, args) with Not_found -> None with
| None -> mkEvar (evk, args)
| Some c -> aux c)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:19:38 +0000