aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-11-05cosmetiqueletouzey
2002-11-04un bug concernant l'expansion des Map_rec si Map n'est pas ouvertletouzey
2002-11-04nettoyage et reorganisationletouzey
2002-11-04maj avec tous les mliletouzey
2002-11-04Un fichier a utiliser via Drop pour le debug de l'extraction.letouzey
2002-11-04ajout d'une entrée au makefile pour faire toutes les theories sauf les realsletouzey
2002-11-04ajout d'un printer pour les global_referenceletouzey
2002-11-03Ajout delimiteurs dans les motifs de Casesherbelin
2002-11-03Moulinetteherbelin
2002-11-03Diversherbelin
2002-11-01majfilliatr
2002-10-31L'extraction c'est magic cvs -n upletouzey
2002-10-31majfilliatr
2002-10-30Désagglutination du squelette de la notation et de sa précédenceherbelin
2002-10-30Optimisation du choix des niveaux intermédiaires dans une notation complexeherbelin
2002-10-29Bugsherbelin
2002-10-29Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-29Mais laisser la syntaxe (!id) aussi disponible !herbelin
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
2002-10-29Parenthèse non obligatoires autour de !id sans argumentherbelin
2002-10-29Prise en compte let-inherbelin
2002-10-29majfilliatr
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-28majfilliatr
2002-10-26code mortherbelin
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...herbelin
2002-10-23Le test de redondance d'une règle était trop fortherbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-22MAJherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-22Correction d'une incompatibilité de nommage introduite lors du commit précÃ...herbelin
2002-10-22majfilliatr
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21Mise en transparence des schémas d'induction bien-fondée sur Setherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-10-21Niveau d'affichage sumor/sumbool incohérent avec le parsingherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-21Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...herbelin
2002-10-21Bug qui empêchait "0" d'être parenthèséherbelin
2002-10-19Meilleure lisibilité grâce à tclTHENLISTherbelin
2002-10-19Réparation bug #180herbelin
2002-10-19Ajout d'infixesherbelin
2002-10-18Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsherbelin
2002-10-17Bugs dans la factorisation des règles de parsing de "{ ... } * ..."herbelin
2002-10-17Moins de restriction sur le commit 1.5herbelin
2002-10-17Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsherbelin