From 0b951b92d3d737fea7f487aadada83d2b7e0d418 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 14 Sep 2022 18:20:10 -0400 Subject: [PATCH] fix some warnings --- src/base/th_data.ml | 1 - src/base/th_lra.ml | 1 - src/core/proof_trace.mli | 2 -- src/sat/store.mli | 1 - src/smt/model_builder.mli | 1 - 5 files changed, 6 deletions(-) diff --git a/src/base/th_data.ml b/src/base/th_data.ml index 1001ce21..87dede54 100644 --- a/src/base/th_data.ml +++ b/src/base/th_data.ml @@ -4,7 +4,6 @@ open Sidekick_core let arg = (module struct - module S = Solver open! Sidekick_th_data open Data_ty module Cstor = Cstor diff --git a/src/base/th_lra.ml b/src/base/th_lra.ml index 933b482e..25c5e587 100644 --- a/src/base/th_lra.ml +++ b/src/base/th_lra.ml @@ -3,7 +3,6 @@ open Sidekick_core module T = Term module Q = Sidekick_zarith.Rational -open LRA_term let mk_eq = Form.eq let mk_bool = T.bool diff --git a/src/core/proof_trace.mli b/src/core/proof_trace.mli index 67ef05cb..b276f1e4 100644 --- a/src/core/proof_trace.mli +++ b/src/core/proof_trace.mli @@ -6,8 +6,6 @@ to its premises. *) -open Sidekick_core_logic - type lit = Lit.t type step_id = Proof_step.id diff --git a/src/sat/store.mli b/src/sat/store.mli index 73be49e3..112f075f 100644 --- a/src/sat/store.mli +++ b/src/sat/store.mli @@ -1,5 +1,4 @@ open Sidekick_core -open Sigs type var = Base_types_.var type atom = Base_types_.atom diff --git a/src/smt/model_builder.mli b/src/smt/model_builder.mli index f149a916..592a73c9 100644 --- a/src/smt/model_builder.mli +++ b/src/smt/model_builder.mli @@ -6,7 +6,6 @@ TODO: seen values? *) -open Sidekick_core open Sigs type t