module Congruence:sig
..end
The congruence stores a finite representation of a set of (ground)
equations an inequalities. It is backtrackable, ie one can go
back to a previous point as long as it is compatible with
a LIFO usage.
module type S =sig
..end
module type TERM =sig
..end
module Make(
T
:
TERM
)
:S
with type term = T.t
module FO:S
with type term = FOTerm.t