diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli index bf22cd28..8fe1838d 100644 --- a/src/core-logic/const.mli +++ b/src/core-logic/const.mli @@ -4,7 +4,6 @@ open Types_ -type t = const type view = const_view = .. module type DYN_OPS = sig @@ -14,6 +13,7 @@ module type DYN_OPS = sig end type ops = (module DYN_OPS) +type t = const = { c_view: view; c_ops: ops; c_ty: term } val view : t -> view val make : view -> ops -> ty:term -> t diff --git a/src/core-logic/sidekick_core_logic.ml b/src/core-logic/sidekick_core_logic.ml index faef37b1..c06f698a 100644 --- a/src/core-logic/sidekick_core_logic.ml +++ b/src/core-logic/sidekick_core_logic.ml @@ -4,9 +4,6 @@ module Bvar = Bvar module Const = Const module Subst = Subst module T_builtins = T_builtins - -(* *) - module Store = Term.Store (* TODO: move to separate library? *)