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 /kernel/nativelambda.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 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 9ed0f6f411..02ee501f5f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -474,7 +474,7 @@ let rec lambda_of_constr cache env sigma c = | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> - let args = Array.map (lambda_of_constr cache env sigma) args in + let args = Array.map_of_list (fun c -> lambda_of_constr cache env sigma c) args in Levar(evk, args) | Some t -> lambda_of_constr cache env sigma t) |