Module Coercion

module Coercion: sig .. end

Support for coercions in the logic language

type t 

a set of coercions

val empty : t
val add : t -> Term.lsymbol -> t

adds a new coercion from function ls: ty1 -> ty2 raises an error if

val find : t -> Ty.ty -> Ty.ty -> Term.lsymbol list

returns the coercion, or raises Not_found

val union : t -> t -> t

union s1 s2 merges the coercions from s2 into s1 (as a new set of coercions) this is asymetric: a coercion from s2 may hide a coercion from s1