diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml index 2c0330eb..cf9f06f6 100644 --- a/src/core-logic/term.ml +++ b/src/core-logic/term.ml @@ -157,10 +157,10 @@ module Store = struct (* TODO: use atomic? CCAtomic? *) let n = ref 0 - let create () : t = + let create ?(size = 256) () : t = let s_uid = !n in incr n; - { s_uid; s_exprs = Hcons.create ~size:256 () } + { s_uid; s_exprs = Hcons.create ~size () } (* check that [e] belongs in this store *) let[@inline] check_e_uid (self : t) (e : term) = diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli index dfb2a65f..66e3e93b 100644 --- a/src/core-logic/term.mli +++ b/src/core-logic/term.mli @@ -99,7 +99,7 @@ val ty : t -> t module Store : sig type t = store - val create : unit -> t + val create : ?size:int -> unit -> t end val type_ : store -> t