Is Coq synthetic or analytic?

Question

In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d

At 33:52, Harper was giving parallel comparison between synthetic theories and analytic ones, and when he reached PL theory, he said Coq is analytic and said Coq only proves a language in its grammar but not the parser itself.

I have a strong desire to disagree somehow but I don't have a clear idea why I would want to do that. I believe that Coq is very synthetic, so are any other proof assistants based on dependent type theory, because all these languages do nothing but build programs. We can also express axiomatic algebra in Coq by using type classes for example, and concretize whenever suitable. This pattern is especially the case in Agda.

So my question is, was Harper right? If he's right, which part of my view causes my misunderstanding?