Cours de Coq

Il y a quelques années, j'ai préparé une collection de vidéos pour un cours introctif de Coq, inspiré du livre Coq'Art que Pierre Castéran et moi-même avons écrit. Ce cours est visible en suivant ce lien.

A la demande de collègues professeurs, je mets également les fichiers tex qui ont servi de sources pour les transparents de ce cours vidéo, à disposition du public, sous couvert d'une licence "CC-Attribution". Comme Coq évolue, il est possible que ces transparents doivent changer pour s'adapter aux nouvelles variantes syntaxiques. J'espère que mes collègues me tiendront au courant des modifications nécessaires.