aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-10-08majcoq
2005-10-07majcoq
2005-10-07Ajout maj répertoire d'archivage par version de Coqherbelin
2005-10-06majcoq
2005-10-06MAJ pauillac -> yquemherbelin
2005-10-05majcoq
2005-10-04majcoq
2005-10-03majcoq
2005-10-02majcoq
2005-10-01majcoq
2005-09-30majcoq
2005-09-29majcoq
2005-09-28majcoq
2005-09-27majcoq
2005-09-26majcoq
2005-09-25majcoq
2005-09-24majcoq
2005-09-23majcoq
2005-09-22majcoq
2005-09-21majcoq
2005-09-21Niveau 99 permettant de parser { } nécessaire aussi dans l'entrée patternherbelin
2005-09-20majcoq
2005-09-19majcoq
2005-09-18majcoq
2005-09-17majcoq
2005-09-16majcoq
2005-09-16changed the syntax categories of arguments of functional schemecoq
2005-09-15majcoq
2005-09-14majcoq
2005-09-13majcoq
2005-09-12majcoq
2005-09-11majcoq
2005-09-10majcoq
2005-09-10Petit bug Declare Implicit Tacticherbelin
2005-09-09majcoq
2005-09-09majcoq
2005-09-09Declare Implicit Tacticherbelin
2005-09-09Declare Implicit Tacticherbelin
2005-09-09Référence pour IntMapherbelin
2005-09-09Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...herbelin
2005-09-09Conséquences nettoyage pretyping.mlherbelin
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...herbelin
2005-09-09Suppression code inactif et commentaire apparemment incorrect (pour éviter c...herbelin
2005-09-09Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...herbelin
2005-09-08majcoq
2005-09-08Test clear final dans intros patternherbelin
2005-09-08Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ...herbelin
2005-09-08Simplification message d'anomalieherbelin
2005-09-08Réparation bug #1004; nettoyageherbelin
2005-09-07majcoq