diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index ef013ccd3..8d255f64f 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -1173,7 +1173,7 @@ let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml = *) module Context = struct - type t = Ses.Equality.t [@@deriving compare, equal, sexp] + type t = Ses.Equality.t [@@deriving sexp] type classes = exp list Term.Map.t let classes_of_ses clss = diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index ba03fa3e5..227a0fbe7 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -169,7 +169,7 @@ end (** Inference System *) module Context : sig - type t [@@deriving compare, equal, sexp] + type t [@@deriving sexp] type classes = Term.t list Term.Map.t val classes : t -> classes diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 9af5becc2..8c9e432bb 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t} type starjunction = { us: Var.Set.t ; xs: Var.Set.t - ; ctx: Context.t + ; ctx: Context.t [@ignore] ; pure: Formula.t ; heap: seg list ; djns: disjunction list }