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 /kernel/reduction.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 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7574d7b21e..4ff90dd70d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -367,9 +367,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect l2r infos el1 el2 - (Array.map (mk_clos env1) args1) - (Array.map (mk_clos env2) args2) cuniv + convert_list l2r infos el1 el2 + (List.map (mk_clos env1) args1) + (List.map (mk_clos env2) args2) cuniv else raise NotConvertible (* 2 index known to be bound to no constant *) @@ -702,6 +702,13 @@ and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = in Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv +and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with +| [], [] -> cuniv +| c1 :: v1, c2 :: v2 -> + let cuniv = ccnv CONV l2r infos lft1 lft2 c1 c2 cuniv in + convert_list l2r infos lft1 lft2 v1 v2 cuniv +| _, _ -> raise NotConvertible + let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in |