Yves Bertot chercheur à l'INRIA, et co-auteur du Coq'Art, a écrit un nombre impressionnant de tutoriels sur Coq, et ses diverses applications en mathématiques et informatique. Cliquez donc ici !
Il y a deux outils pour travailler en Coq.
Pour les habitués d'Emacs : utiliser Proof General (voir note en bas de page), qui est un mode Emacs spécialisé dans les preuves interactives.
Ceux qui préfèrent les "ide" , utiliser coqide, l'environnement de développement intégré pour Coq.
coqide est moins usine à gaz qu'Eclipse.
Si un bug provoqué par la diabolique touche MOD4 (celle avec une fenêtre tordue) de votre clavier se produit, alors
éditer votre fichier $HOME/.coqiderc et remplacer toutes les occurrences de
MOD4 par MOD1, puis relancer.