diff options
| author | Pierre-Marie Pédrot | 2018-09-28 18:55:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-06 14:51:54 +0200 |
| commit | 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 (patch) | |
| tree | 7bc43cb8e9561e1355ad99ddd0f10004e1bdf7d4 /engine/eConstr.ml | |
| parent | 2089207415565e8a28816f53b61d9292d04f4c59 (diff) | |
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.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 4 |
1 files changed, 2 insertions, 2 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) |