module Binder : sig ... endmodule Builtin : sig ... endmodule Cnf : sig ... endmodule Comparison : sig ... endmodule Compute_prec : sig ... endmodule Congruence : sig ... endmodule Congruence_intf : sig ... endThe 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 DBEnv : sig ... endmodule Defined_pos : sig ... endmodule Dtree : sig ... endmodule FV_tree : sig ... endmodule FeatureVector : sig ... endmodule Fingerprint : sig ... endmodule FixpointUnif : sig ... endmodule Flex_state : sig ... endmodule HO_unif : sig ... endmodule HVar : sig ... endmodule Hash : sig ... endmodule Hashcons : sig ... endmodule IArray : sig ... endmodule ID : sig ... endmodule Ind_ty : sig ... endmodule Index : sig ... endmodule Index_intf : sig ... endmodule InnerTerm : sig ... endmodule Input_format : sig ... endmodule Interfaces : sig ... endmodule JPFull : sig ... endmodule JP_unif : sig ... endmodule Lambda : sig ... endmodule LazyList : sig ... endmodule Literal : sig ... endmodule Literals : sig ... endmodule Multiset : sig ... endmodule Multiset_intf : sig ... endmodule Multisets : sig ... endmodule NPDtree : sig ... endmodule Options : sig ... endmodule Ordering : sig ... endmodule Output_format : sig ... endmodule PUnif : sig ... endmodule ParseLocation : sig ... endmodule PatternUnif : sig ... endmodule Polynomial : sig ... endmodule Position : sig ... endmodule PragUnifParams : sig ... endmodule Precedence : sig ... endmodule PrefWeight : sig ... endmodule Proof : sig ... endmodule Rewrite : sig ... endmodule SLiteral : sig ... endmodule STerm : sig ... endmodule Scoped : sig ... endmodule Signal : sig ... endmodule Signature : sig ... endmodule Skolem : sig ... endmodule SolidSubsumption : sig ... endmodule SolidUnif : sig ... endmodule Statement : sig ... endmodule Subst : sig ... endmodule Term : sig ... endmodule Type : sig ... endmodule TypeInference : sig ... endmodule TypedSTerm : sig ... endmodule Unif : sig ... endmodule UnifFramework : sig ... endmodule Unif_constr : sig ... endmodule Unif_intf : sig ... endmodule Unif_subst : sig ... endmodule UntypedAST : sig ... endmodule Util : sig ... endmodule Var : sig ... endmodule ZProf : sig ... end