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/clambda.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/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 8c7aa6b17a..65de52c0f6 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -670,7 +670,7 @@ let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") | Evar (evk, args) -> - let args = lambda_of_args env 0 args in + let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in Levar (evk, args) | Cast (c, _, _) -> lambda_of_constr env c @@ -799,9 +799,6 @@ and lambda_of_args env start args = (fun i -> lambda_of_constr env args.(start + i)) else empty_args - - - (*********************************) let dump_lambda = ref false |