module Sort : sig ... endmodule Value : sig ... endmodule Term : sig ... endmodule Inductive : sig ... endmodule Operator : sig ... endmodule Gamma : sig ... endmodule Typecheck : sig ... endmodule Name_map : sig ... endmodule Context : sig ... endmodule Unifier : sig ... endmodule Gamma_holes : sig ... endGamma_holes is a context with holes which can be filled later. A hole is a local unnamed variable with a type (i.e. an assumption that an element with this type exists), initially without value. Later on the value can be provided.
module Gamma_algo : sig ... endmodule Term_printer : sig ... endmodule Print_inductive : sig ... end