cours-coq-Bertot-2009

Updated source code for Cours Vidéo de Coq 2009 by Yves Bertot.

Original code by Yves Bertot is modified where needed to compile with Coq 8.9

cours-coq-Bertot-2009 is an EDLA project.

The purpose of edla.org is to promote the state of the art in various domains.

Coq 8.9 or later

Name		Name	Last commit message	Last commit date
Latest commit History 21 Commits
ch1.1-les_fonctions_en_Coq		ch1.1-les_fonctions_en_Coq
ch1.11-nombres_naturels_et_recursion		ch1.11-nombres_naturels_et_recursion
ch1.12-valeurs_booleennes_couples_et_listes		ch1.12-valeurs_booleennes_couples_et_listes
ch1.5-l_ordre_superieur		ch1.5-l_ordre_superieur
ch1.6-les_structures_de_donnees_en_Coq		ch1.6-les_structures_de_donnees_en_Coq
ch1.8-types_inductifs_en_Coq		ch1.8-types_inductifs_en_Coq
ch2.2-faire_des_preuves_en_Coq		ch2.2-faire_des_preuves_en_Coq
ch2.3-preuves_avec_les_connecteurs_logiques		ch2.3-preuves_avec_les_connecteurs_logiques
ch2.6-premieres_preuves_de_programmes		ch2.6-premieres_preuves_de_programmes
ch3.1-introduction_aux_proprietes_inductives_en_Coq		ch3.1-introduction_aux_proprietes_inductives_en_Coq
ch3.4-inversion_des_proprietes_inductives		ch3.4-inversion_des_proprietes_inductives
ch4.3-le_polymorphisme		ch4.3-le_polymorphisme
ch5.2-famille_de_types_recursifs_heterogenes		ch5.2-famille_de_types_recursifs_heterogenes
ch5.3-principe_de_recurrence_pour_les_predicats_inductifs		ch5.3-principe_de_recurrence_pour_les_predicats_inductifs
ch6.1-valeurs_certifiees		ch6.1-valeurs_certifiees
ch7.1-recursion_generale		ch7.1-recursion_generale
ch7.2-relations_bien_fondees		ch7.2-relations_bien_fondees
ch7.3-la_commande_Function		ch7.3-la_commande_Function
.gitignore		.gitignore
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
_CoqProject		_CoqProject

Provide feedback