The C-zar declarative proof language for Coq is part of the standard Coq distribution as of version 8.1 .
As of version 8.2, the Coq Reference manual contains a section about the C-zar language.
Please check the file sqrt2.v for an sample.
A detailed description of the declarative proof language is the basis for this article.