sig val typ : Coq.lazy_ref val of_int : int -> EConstr.constr end