From c873346047a1b484a59f92f510542f45447a11a2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 5 Aug 2022 21:56:45 -0400 Subject: [PATCH] detail in th-lra --- src/th-lra/sidekick_th_lra.ml | 4 +--- src/th-lra/sidekick_th_lra.mli | 5 +++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml index d1666f2d..5d60f300 100644 --- a/src/th-lra/sidekick_th_lra.ml +++ b/src/th-lra/sidekick_th_lra.ml @@ -4,11 +4,9 @@ open Sidekick_core open Sidekick_cc module Intf = Intf -open Intf +include Intf module SI = SMT.Solver_internal -module type ARG = Intf.ARG - module Tag = struct type t = Lit of Lit.t | CC_eq of E_node.t * E_node.t diff --git a/src/th-lra/sidekick_th_lra.mli b/src/th-lra/sidekick_th_lra.mli index fdb34b33..11ee0b4c 100644 --- a/src/th-lra/sidekick_th_lra.mli +++ b/src/th-lra/sidekick_th_lra.mli @@ -1,9 +1,10 @@ (** Linear Rational Arithmetic *) module Intf = Intf -open Intf -module type ARG = Intf.ARG +include module type of struct + include Intf +end (* TODO type state