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 /pretyping/vnorm.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 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index d4da93cc5b..37c34d55cf 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -205,7 +205,7 @@ and nf_evar env sigma evk stk = let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma @@ Evd.evar_concl evi in if List.is_empty hyps then - nf_stk env sigma (mkEvar (evk, [||])) concl stk + nf_stk env sigma (mkEvar (evk, [])) concl stk else match stk with | Zapp args :: stk -> (* We assume that there is no consecutive Zapp nodes in a VM stack. Is that @@ -217,6 +217,7 @@ and nf_evar env sigma evk stk = let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in let inst, args = Array.chop (List.length hyps) args in + let inst = Array.to_list inst in let c = mkApp (mkEvar (evk, inst), args) in nf_stk env sigma c t stk | _ -> |