They probably mean that bringing dependent types into a programming language, proper, partially obviates the need for Coq and similar systems since it renders t

They probably mean that bringing dependent types into a programming language, proper, partially obviates the need for Coq and similar systems since it renders them (at least partially) redundant. Having dependent types, and having mechanics in-language to produce proofs, would cover a large part of what people (who are producing programs and not focused strictly on the theorem proving side for other purposes) are using Coq & others for.