Le langage de preuves déclaratif C-zar pour Coq est inclus dans la distribution standard de Coq depuis la version 8.1 .
Depuis la version 8.2, le Manuel de Référence de Coq contient une section consacrée au langage C-zar.
Vous pouvez avoir un aperçu dans le fichier d'exemple sqrt2.v.
Une description détaillée de la sémantique du langage de preuve déclaratif est disponible dans cet article.