CRGTCoq20101217

Date : vendredi 17 décembre 2010

Heure : 14h–17h

Lieu : INRIA Place d'Italie, salle orange 2

Présents

• Pierre Boutillier
• Pierre Courtieu
• Julien Forest
• Stéphane Glondu
• Hugo Herbelin
• Pierre Letouzey
• Yann Régis-Gianas
• Matthieu Sozeau

Préparation de la 8.3pl1

• nécessaire au moins pour les tactiques de compatibilité 8.2 (constr_eq, is_evar) et pour la compatibilité camlp5 6.02
• bouclage mardi 21/12, tag à partir de mercredi matin (à voir avec Jean-Marc)
• Matthieu s'occupe du bench
• Pierre L. fait le paquet Windows
• Pierre B. refera un paquet Mac Coqide (et automatisera sa construction)

Exposé de Pierre L sur les nombres

• L'exposé : expose-gt-letouzey-nombres.txt
• Quelques discussions sur la représentations de n/0. La conclusion pratique de Pierre : on s'attend à ce que la définition concrète ait une valeur par défaut mais l'interface ne spécifie rien sur cette valeur. Cette approche permet par exemple de considérer que 0 * (p / 0) est bien défini et toujours égal à 0.

Divers

• Pierre B. ajouter la possibilité de prévoir la place des paramètres des constructeurs dans les clauses de filtrage de match afin de rétablir une symétrie entre motifs et termes
• Qed using section_hyps et Admitted using section_hyps ont été rediscutés dans l'optique de permettre une précompilation sans vérification des preuves en présences de variables de section.