CR FOST Réunion du 19 juin 2009 à Villetaneuse Participants: Yves Bertot, Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Milad Niqui, Iona Pasca. * exposé M Niqui - il existe différentes axiomatisations des réels en Coq => trouver une axiomatisation minimale commune à toutes Ainsi, il suffira d'ajouter quelques axiomes différents à chaque fois pour arriver sur les axiomatisations existantes => créer Preal (les pre-real ou les propositionnal real) tel que Preal soit inclus dans CorN qui est inclus dans la bibliothèque standard * exposé S Boldo sur CerPAN et FOST questions sur les apports de ssreflect et sur la définition du O * discussions sur Gappa avec G Melquiond * exposés de I Pasca - réels, vecteurs et matrices de réels en ssreflect - méthode de Newton certifiée