aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2001-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
2001-06-27Reduction tres significative du terme preuvedelahaye
2001-06-26Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous uneclrenard
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-25liste des equiv exporteeclrenard
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
2001-06-20Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...clrenard
2001-06-19Un bug corrige.clrenard
2001-06-12Ajout de la tactique Setoid_replace.clrenard
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-28Pretty -> Prettypfilliatr
2001-05-28patch Claudiofilliatr
2001-05-28nettoyagefilliatr
2001-05-25Oups: flingait les Dglob dans optimizeletouzey
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-22majletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 12:10:50 +0000