Are there any declarative proof languages for Coq?

[brando90]

discussion of Czar, a (currently unsupported) declarative language for Coq:

What is the difference between SSReflect and Czar?

IMHO I’d expect the opposite, but I don’t actually know. Historically, Isabelle has more automation, and part of the reason is that its automation can execute faster. OTOH, Coq has a more expressive logic and type system — try writing an Isabelle type for the elements of an n-dimensional vector space.