aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-12-21Passage coqwebherbelin
2001-12-21Commentaire coqweb non ferméherbelin
2001-12-21MAJ V7.2herbelin
2001-12-21Extension de Evenherbelin
2001-12-21Extension de Even et Div2herbelin
2001-12-21*** empty log message ***herbelin
2001-12-21Ajout d'un exemple de Christineherbelin
2001-12-21Bug affichage '++' au lieu de ';'herbelin
2001-12-21*** empty log message ***courant
2001-12-21comment faire le .debcourant
2001-12-21preparation V7.2courant
2001-12-21paquet Debiancourant
2001-12-21maj CHANGES extraction + bug extraction & _letouzey
2001-12-20MAJherbelin
2001-12-20Convertibilité au lieu d'alpha-équivalence pour les motifs non linéaires d...herbelin
2001-12-20Mise en place de la réduction sous forme d'implications d'atomes en fn de têteherbelin
2001-12-20Utilisation de Hnf plutôt que Redherbelin
2001-12-20Non dépliage des Fix non réductibles dans Hnfherbelin
2001-12-20Code mortherbelin
2001-12-19Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelseherbelin
2001-12-19Test sobriété de la réduction de Intuitionherbelin
2001-12-19Test sobriété de la réduction de Intuitionherbelin
2001-12-19MAJherbelin
2001-12-19Bug de de Bruijn pour le LetInherbelin
2001-12-19Insertion de Red sur chaque atome dans Tauto et Intuitionherbelin
2001-12-19suppression de commentaires obsoletesletouzey
2001-12-19contrib/interface/dad.ml4 had no real need of streams, it should have beenbertot
2001-12-19debranchement du test sur les Realsletouzey
2001-12-19*** empty log message ***desmettr
2001-12-19Changements Realsdesmettr
2001-12-19Modif précédente trop violente (cf test-suite/success/CasesDep.v)herbelin
2001-12-19Tentative d'amélioration du résultat de Intuitionherbelin
2001-12-19Pour les développeurs extérieursherbelin
2001-12-19MAJ Grammarherbelin
2001-12-19MAJ 7.2herbelin
2001-12-19MAJ 7.2herbelin
2001-12-19MAJ nombre magiqueherbelin
2001-12-19reparation du make depend et du .dependletouzey
2001-12-19MAJherbelin
2001-12-19Corrections post contournement des streams avec ++herbelin
2001-12-19Réorganisationherbelin
2001-12-19Pour les développeurs extérieursherbelin
2001-12-19MAJ V7.2herbelin
2001-12-19MAJherbelin
2001-12-19MAJherbelin
2001-12-19NatRing (2ème)herbelin
2001-12-19NatRingherbelin
2001-12-19Le cas LetIn avait été oublié dans case_branches_specifherbelin
2001-12-19Un peu plus d'inférence des ? traitée par le Casesherbelin
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ...herbelin