Module Unif


module Unif: sig .. end

Unification



val unif : (Term.term * Term.term) list -> Subs.subs
Return mgu or raise Failure
val mgu : Term.term -> Term.term -> Subs.subs
Computes the MGU of two terms.