diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml index 3cbce44d8..f0fd2ae9c 100644 --- a/sledge/src/fol/arithmetic.ml +++ b/sledge/src/fol/arithmetic.ml @@ -305,11 +305,6 @@ struct let trms poly = Iter.flat_map ~f:Mono.trms (monos poly) - type product = Prod.t - - let fold_factors = Prod.fold - let fold_monomials = Sum.fold - (* query *) let vars p = Iter.flat_map ~f:Trm.vars (trms p) diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml index 50187ac9e..fe99f475e 100644 --- a/sledge/src/fol/arithmetic_intf.ml +++ b/sledge/src/fol/arithmetic_intf.ml @@ -71,13 +71,6 @@ module type S = sig (** [solve_zero_eq d] is [Some (e, f)] if [0 = d] can be equivalently expressed as [e = f] for some monomial subterm [e] of [d]. If [for_] is passed, then the subterm [e] must be [for_]. *) - - (**/**) - - type product - - val fold_factors : product -> 's -> f:(trm -> int -> 's -> 's) -> 's - val fold_monomials : t -> 's -> f:(product -> Q.t -> 's -> 's) -> 's end (** Indeterminate terms, treated as atomic / variables except when they can