Is Coq synthetic or analytic?
The remark is about one specific usage of Coq, namely formalization of programming language theory.

Let us first make clear the distinction between synthetic and analytic:


In a synthetic approach to a subject we say that there are things whose basic properties and structure are postulated in one way or another. We then study these things by relying only on the postulated properties and structure.
In an analytic approach to a subject we discover that there are certain things. To learn more about them, we take them apart, we study how they are made and we analze them. This way we discover their properties and structure.


How would one study a programming language in these two ways?

Synthetically, we would postulate the constituent parts of the language (there are terms, there are types), their basic structure (these are the ways of building terms) and basic properties. We do not ask what the terms and type are made of, or whether the terms are trees or strings, or whether the collection of types is built in a particular way.

Analytically, we would start with a mathematical setup that allows us to do many things, such as use inductive definitions to construct mathematical objects. We woudl build terms and types as particular inductively defined sets or types. Then we would study their structure, how we can transform them, etc.

It should be clear that Coq is of the analytic kind. When you implement a programming language in Coq, you define inductive types of terms and types. Then you analyze them using induction, define operational semantics as a recursive function on the syntax of terms, etc.

On the other hand, Twelf is of the synthetic kind. We postulate that there is a type of terms and a type of types, but we do not tell Twelf that these are inductive types (there's no way to say that in Twelf). We define operational semantics by providing basic transition rules. There is no mention of recursively defined functions (there's no way to define functions in Twelf), we just rely on the postulates that we wrote down.

You should compare the above situation to planar geometry. Hilbert's approach to geometry is synthetic (but his ideas are rooted in Euclid), Descartes' are analytic. The analytic geometry is so called because a line is not a primitive concepts: it has an inner structure, namely it is a set of points.