aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-10-15pattern-matching avec cas inutilise dans closurebarras
2002-10-15commit du calcul des dependances un peu plus robustebarras
2002-10-15majfilliatr
2002-10-14MAJ pour NewtonIntdesmettr
2002-10-14Integrale de Newtondesmettr
2002-10-14*** empty log message ***desmettr
2002-10-14TacCall attend une référenceherbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-14Réparation bug Inversion (#212)herbelin
2002-10-14Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pasherbelin
2002-10-14Ajout optino_iterherbelin
2002-10-14Parenthèses forcées autour des arguments d'une application pour parserherbelin
2002-10-14La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-14coqdep bogué, retour sur version 1.75herbelin
2002-10-14majfilliatr
2002-10-13Bug affichage du chiffre 0herbelin
2002-10-13MAJherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-13Moins de restriction sur le commit précédentherbelin
2002-10-13Ajout map_rawconstrherbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-10-13Nettoyageherbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-12réparation de la protection contre les clauses indiscernables de TACTIC EXTE...herbelin
2002-10-12Notation 2:Check et 2:Evalherbelin
2002-10-12Restriction sur la forme des Syntactic Definition et re-localisation en fonct...herbelin
2002-10-12Nettoyageherbelin
2002-10-12Forcer la réouverture d'un fichier explicitement requis même si leherbelin
2002-10-11majfilliatr
2002-10-10Ajout ClassicalFactsherbelin
2002-10-10gestion coherente de l'option -R et des Require A.B.C.barras
2002-10-10Nametab permet de definir le meme truc la deuxieme foiscoq
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-10-09Preuve du lemme de Rolledesmettr
2002-10-09MAJ pour modification dans Rcompletdesmettr
2002-10-09Suppression d'un lemme redondantdesmettr
2002-10-09Proof of Heine's theoremdesmettr
2002-10-09majfilliatr
2002-10-08Subst ne fait pas clear sur x:=efilliatr
2002-10-08majfilliatr
2002-10-07Une fonction de moins dans .mlicoq
2002-10-07Lazy manuelles dans le codecoq
2002-10-07*** empty log message ***desmettr
2002-10-07*** empty log message ***courant
2002-10-07Quelques resultats complementairesdesmettr
2002-10-07Affaiblissement des hypotheses dans TAF_gendesmettr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:55:08 +0000