diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index d081e04b7..fa7e67cdf 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -31,7 +31,7 @@ module rec Term : sig type t [@@deriving compare, equal, sexp] (* pretty-printing *) - val ppx : Var.strength -> t pp + val ppx : Var.t Var.strength -> t pp val pp : t pp module Map : Map.S with type key := t @@ -104,7 +104,7 @@ and Formula : sig val project : Term.t -> t option (* pretty-printing *) - val ppx : Var.strength -> t pp + val ppx : Var.t Var.strength -> t pp val pp : t pp (** Construct *) @@ -170,7 +170,7 @@ module Context : sig val pp : t pp val ppx_diff : - Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool + Var.t Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool include Invariant.S with type t := t diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli index 4b2d63dde..e78b955cb 100644 --- a/sledge/src/ses/equality.mli +++ b/sledge/src/ses/equality.mli @@ -22,7 +22,7 @@ val classes : t -> classes val pp : t pp val pp_classes : t pp -val ppx_classes : Var.strength -> classes pp +val ppx_classes : Var.t Var.strength -> classes pp include Invariant.S with type t := t diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index d5a1caefb..ae39a60c4 100644 --- a/sledge/src/ses/term.mli +++ b/sledge/src/ses/term.mli @@ -106,7 +106,7 @@ module Map : sig val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t end -val ppx : Var.strength -> t pp +val ppx : Var.t Var.strength -> t pp val pp : t pp val pp_diff : (t * t) pp val invariant : t -> unit diff --git a/sledge/src/ses/var0.ml b/sledge/src/ses/var0.ml index 0004be251..01a1b8c58 100644 --- a/sledge/src/ses/var0.ml +++ b/sledge/src/ses/var0.ml @@ -11,7 +11,7 @@ open Var_intf module Make (T : REPR) = struct include T - type strength = t -> [`Universal | `Existential | `Anonymous] option + type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option let ppx strength ppf v = let id = id v in diff --git a/sledge/src/ses/var_intf.ml b/sledge/src/ses/var_intf.ml index a646ad63c..7ddb070ff 100644 --- a/sledge/src/ses/var_intf.ml +++ b/sledge/src/ses/var_intf.ml @@ -15,9 +15,9 @@ end module type VAR = sig type t [@@deriving compare, equal, sexp] - type strength = t -> [`Universal | `Existential | `Anonymous] option + type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option - val ppx : strength -> t pp + val ppx : t strength -> t pp val pp : t pp module Map : sig @@ -27,11 +27,13 @@ module type VAR = sig end module Set : sig + type var := t + include NS.Set.S with type elt := t val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t - val ppx : strength -> t pp + val ppx : var strength -> t pp val pp : t pp val pp_xs : t pp end