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