• Quelques aspects juridiques liés à Coq
• Avenir de la liste de développement Coq-dev
• Utilisation de Git
• Nouveau Coqdoc
• Arnaud : nouveau moteur
• Discussion générale sur l'implémentation des tactiques.
• Benjamin Grégoire : Ajout des entiers natifs et des tableaux dans Coq.
• Motivation
• Representation des tableaux
• Verification des traces SAT en Coq
• Representation actuelle des entiers machines
• Une premiere solution
• Les chaines de resolution sont representees par des listes
• Solution mise en place (travail en cours)
• Modification des fonctions de reductions
• Quelques remarques
• Difficultes particuliere pour les tableaux
• Des questions pour vous
• Declaration des primitives
• Notations