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 /user-contrib | |
| 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 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 72df4d75c8..783974ebe2 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -375,7 +375,7 @@ let () = define1 "constr_kind" constr begin fun c -> | Evar (evk, args) -> v_blk 3 [| Value.of_int (Evar.repr evk); - Value.of_array Value.of_constr args; + Value.of_array Value.of_constr (Array.of_list args); |] | Sort s -> v_blk 4 [|Value.of_ext Value.val_sort s|] @@ -469,7 +469,7 @@ let () = define1 "constr_make" valexpr begin fun knd -> | (3, [|evk; args|]) -> let evk = Evar.unsafe_of_int (Value.to_int evk) in let args = Value.to_array Value.to_constr args in - EConstr.mkEvar (evk, args) + EConstr.mkEvar (evk, Array.to_list args) | (4, [|s|]) -> let s = Value.to_ext Value.val_sort s in EConstr.mkSort (EConstr.Unsafe.to_sorts s) @@ -603,7 +603,7 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c -> thaw c >>= fun _ -> Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () -> let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in - let args = Array.of_list (EConstr.mkRel 1 :: args) in + let args = EConstr.mkRel 1 :: args in let ans = EConstr.mkEvar (evk, args) in let ans = EConstr.mkLambda (Context.make_annot (Name id) Sorts.Relevant, t, ans) in return (Value.of_constr ans) |