sig type pack = { ar : Term.constr; value : Term.constr; morph : Term.constr; } val typ : Term.constr lazy_t val mk_pack : Coq.Relation.t -> Theory.Sym.pack -> Term.constr val null : Coq.Relation.t -> Term.constr end