aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-10Finalement PolyListSyntax est necessaire (la redondance venait d'une confusio...herbelin
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-09Amélioration message d'erreur arg explicité au lieu d'arg normalherbelin
2000-11-09Renommage canonique SectionLocalDecl -> SectionLocalAssumherbelin
2000-11-09Bug et simplification nouvel Inductionherbelin
2000-11-09do_Makefile -> coq_makefile pour le bootstrap!filliatr
2000-11-09do_Makefile -> coq_makefilefilliatr
2000-11-09-I states dans les includes de Coqfilliatr
2000-11-09-I theories/Init pour faire initial.coqfilliatr
2000-11-09coqc appele avec -bindir binfilliatr
2000-11-09mise a jourfilliatr
2000-11-09all_subdirs teste si son argument est un repertoire; sinon ne fait rienfilliatr
2000-11-08nouveau load pathfilliatr
2000-11-08améliorationherbelin
2000-11-08merge_locherbelin
2000-11-08Insertion de coercion au milieu des applications partielles et propagation de...herbelin
2000-11-08First version with out_variable used. Exports all the standard librarysacerdot
2000-11-08binaires a ingorer par CVSfilliatr
2000-11-08tous les binaires maintenant dans le repertoire binfilliatr
2000-11-08out_variable (Liboject.obj -> ...) distibgue de get_variablefilliatr
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-07Bug sur précédent commitherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-07MAJherbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-11-07Correction sur commit errone de la version 1.3herbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-11-07Orthographeherbelin
2000-11-07MAJherbelin
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06print_idl inlinéherbelin
2000-11-06MAJherbelin
2000-11-06Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-05MAJherbelin
2000-11-05Nouveau mode de compilation de .ml4herbelin
2000-11-05Plus besoin de débrancher la preuve qui ne passait pasherbelin
2000-11-05Plus besoin de rajouter "Require Plus"herbelin
2000-11-05Pour ne plus éviter temporairement le "Auto with zarith" !herbelin
2000-11-05MAJherbelin
2000-11-05Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...herbelin
2000-11-03Deplacement d'options avec ou sans argtsmohring
2000-11-03Few OCaml files in contrib/xmlsacerdot
2000-11-03compilation avec make de Solaris; README et INSTALLfilliatr
2000-11-03URI problem addressed, but not resolved yetsacerdot
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 05:34:48 +0000