Mode d'emploi des exercices : télécharger les fichiers en gardant l'extension .v; ils contiennent toutes les déclarations nécessaires. Les textes des exercices sont dans les commentaires.
Note : Il y aura toujours plus d'exercices que ce qu'on peut faire normalement en une séance de TD. Les solutions seront publiées le mercredi au
plus tard, et pourront être discutées le TD suivant.
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.