aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* correction de bugs:Gravatar barras2002-08-16
* Encore quelques tests sur modules...Gravatar coq2002-08-16
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Test for redundant clausesGravatar herbelin2002-08-15
* Test affichage optimal des coercionsGravatar herbelin2002-08-14
* MAJ depend.coqGravatar coq2002-08-14
* AutoRewrite substitutive...Gravatar coq2002-08-13
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* RenoncementGravatar herbelin2002-08-13
* Petites corrections ici et laGravatar coq2002-08-13
* Preuves dans CC deGravatar herbelin2002-08-13
* En attendant la 3.06, remplacement de +camlp4 par CAMLLIB/camlp4Gravatar herbelin2002-08-02
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* MAJ pour TAFGravatar desmettr2002-07-31
* Theoreme des accroissements finis generalises et corollairesGravatar desmettr2002-07-31
* *** empty log message ***Gravatar desmettr2002-07-31
* MAJ pour Exp_propGravatar desmettr2002-07-31
* Proprietes de l'exponentielleGravatar desmettr2002-07-31
* *** empty log message ***Gravatar desmettr2002-07-31
* Réparation d'un bug qui considérait les composantes d'un QUALIDGravatar herbelin2002-07-30
* Branchement de Assert, Pose et LetTac sur l'algo de création de nomsGravatar herbelin2002-07-30
* MAJ pour Rtrigo_regGravatar desmettr2002-07-29
* Regularite de sin et cosGravatar desmettr2002-07-29
* Continuite des series de fonctions NCGravatar desmettr2002-07-29
* *** empty log message ***Gravatar desmettr2002-07-29
* Ajout d'un point d'entree pour exporter les arbres de preuves en XMLGravatar herbelin2002-07-24
* reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeGravatar letouzey2002-07-24
* suppression des ./ dans les noms des librairiesGravatar barras2002-07-24
* MAJ commentairesGravatar herbelin2002-07-23
* *** empty log message ***Gravatar desmettr2002-07-22
* Quelques ameliorations dans RegGravatar desmettr2002-07-22
* Nvll preuves R_dist_tri et tech_limitGravatar mayero2002-07-19
* correction bugs TautoGravatar courant2002-07-19
* Regularites de pow et des sommes finies / MAJ RegGravatar desmettr2002-07-19
* Resultats de regularite de Rabsolu / MAJ de RegGravatar desmettr2002-07-19
* Quelques ameliorations...Gravatar desmettr2002-07-19
* *** empty log message ***Gravatar desmettr2002-07-18
* Correction d'un bug dans IsCont_ptGravatar desmettr2002-07-18
* MAJ pour Sqrt_regGravatar desmettr2002-07-18
* Preuves de la continuite/derivabilite de sqrt sur R+/R+*Gravatar desmettr2002-07-18
* *** empty log message ***Gravatar desmettr2002-07-18
* reparation temporaire(?) a coup de MLdummy'Gravatar letouzey2002-07-17
* tactique SubstGravatar filliatr2002-07-17
* Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]Gravatar corbinea2002-07-17
* ajout de make otags utilisant otags plutot que etagsGravatar letouzey2002-07-17
* modification de make tags pourGravatar letouzey2002-07-17
* majGravatar letouzey2002-07-16
* Pour ocamlwebGravatar letouzey2002-07-16
* Souci avec example fbidon...Gravatar letouzey2002-07-16