CRGTCoq20101217 - coq/coq GitHub Wiki

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.
⚠️ **GitHub.com Fallback** ⚠️