CRGTCoq20101217

Pierre Letouzey edited this page Oct 18, 2017 · 7 revisions

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.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.