Are there any declarative proof languages for Coq?

I was interested in declarative proof languages for Coq. Is this possible?

Only reference I know of: