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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/goal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index b1f8fd3e97..53d3047bc7 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -69,7 +69,7 @@ module V82 = struct let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) |