aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2001-10-29Oups: un relicat de fn de cacheletouzey
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...letouzey
2001-10-25correctif bug des de Bruijn du Double Caseletouzey
2001-10-24seisme suite. correction bugsletouzey
2001-10-24Patch de goption.ml pour faire marcher les options synchrones. Passage des op...letouzey
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-10-23suite du seismeletouzey
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...letouzey
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-12reparationfilliatr
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-01correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...letouzey
2001-09-21Correction due au changement de semantique de Matchdelahaye
2001-09-20Transparentbarras
2001-09-20correction du eta_expanseletouzey
2001-09-20Report des modifs de Claudioherbelin
2001-09-20bug affichage des termes ml fournisletouzey
2001-09-20utilisation du nouveau get_sort_family_ofletouzey
2001-09-20changements mineurs du testletouzey
2001-09-20Romegamohring
2001-09-19ajout du fichier CHANGESletouzey
2001-09-19adaptation a la nouvelle syntaxe Extract Inlined Constantletouzey
2001-09-19Changements de Extraction truc et Recursive Extractionletouzey
2001-09-19Deux nouvelles optimisations pour Casesletouzey
2001-09-19MAJ V7.1herbelin
2001-09-19Verification supplementaire avant optimisation singletonletouzey
2001-09-19reparation Znemohring
2001-09-18travail sur le Extract Constantletouzey
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
2001-09-18Romega/names/Makefilemohring
2001-09-14MAJ vis à vis de la nouvelle non-localité des Remark/Factherbelin
2001-09-12*** empty log message ***mohring
2001-09-10changement du make depend en vu du make realsletouzey
2001-09-10bug de rename_global modulaire corrige'letouzey
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-08-10Prsingherbelin
2001-08-10Parsingherbelin
2001-08-07Passage au nouveau Destructherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...herbelin
2001-07-18Ajout de la contrib sur les graphesmohring
2001-07-10Setoid_rewrite -> Rewriteclrenard
2001-07-10Ajout des fichiers pour le Ring pour setoidesclrenard
2001-07-10Changement de place de la tactique Setoid_rewriteclrenard
2001-07-10Ajout d'un Ring pour setoidesclrenard
2001-07-05correction bug Omegafilliatr
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-06-27Reduction du terme preuve fourni par Fielddelahaye