diff options
| author | Maxime Dénès | 2020-04-21 13:21:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-04-21 13:21:09 +0200 |
| commit | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (patch) | |
| tree | 6009d4f34f3af2923de51ee853d2085b1d657200 /engine/eConstr.ml | |
| parent | 2fdca75132b7d8495b7df5b10bbd9dde05fd5190 (diff) | |
| parent | e89cf30983d3af97607885413a4a8eaaa071fa52 (diff) | |
Merge PR #11896: Use lists instead of arrays in evar instances.
Ack-by: SkySkimmer
Reviewed-by: maximedenes
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) |