aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Cablage des syntactif defs avec la Nametab des objetsGravatar herbelin2000-11-20
* Mieux à sa place dans toplevelGravatar herbelin2000-11-20
* Prise en compte noms longsGravatar herbelin2000-11-20
* Ajout pr_global_reference et is_visibleGravatar herbelin2000-11-20
* Tables des eval_constant devient une CstmapGravatar herbelin2000-11-20
* Une capsule pour save_module_to dans DischargeGravatar herbelin2000-11-20
* mise a jourGravatar filliatr2000-11-15
* Changed the semantics of AddRecPath.Gravatar sacerdot2000-11-15
* methode exportGravatar filliatr2000-11-15
* -opt ne remplace plus camlp4 par camlp4o.opt car on ne peut pasGravatar filliatr2000-11-15
* concernant les binairesGravatar filliatr2000-11-15
* Retour a la version 1.1Gravatar herbelin2000-11-13
* Y avait des '.' non suivis d'un séparateurGravatar herbelin2000-11-11
* Gros hack pour afficher les universGravatar herbelin2000-11-11
* Code more concernant feu les abstractionsGravatar herbelin2000-11-11
* Prise en compte camlp4.opt dans la configuration et le MakefileGravatar herbelin2000-11-11
* mise-a-jour, ajouts de quelques truc...Gravatar mayero2000-11-10
* Code mortGravatar herbelin2000-11-10
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Finalement PolyListSyntax est necessaire (la redondance venait d'une confusio...Gravatar herbelin2000-11-10
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Amélioration message d'erreur arg explicité au lieu d'arg normalGravatar herbelin2000-11-09
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* Bug et simplification nouvel InductionGravatar herbelin2000-11-09
* do_Makefile -> coq_makefile pour le bootstrap!Gravatar filliatr2000-11-09
* do_Makefile -> coq_makefileGravatar filliatr2000-11-09
* -I states dans les includes de CoqGravatar filliatr2000-11-09
* -I theories/Init pour faire initial.coqGravatar filliatr2000-11-09
* coqc appele avec -bindir binGravatar filliatr2000-11-09
* mise a jourGravatar filliatr2000-11-09
* all_subdirs teste si son argument est un repertoire; sinon ne fait rienGravatar filliatr2000-11-09
* nouveau load pathGravatar filliatr2000-11-08
* améliorationGravatar herbelin2000-11-08
* merge_locGravatar herbelin2000-11-08
* Insertion de coercion au milieu des applications partielles et propagation de...Gravatar herbelin2000-11-08
* First version with out_variable used. Exports all the standard libraryGravatar sacerdot2000-11-08
* binaires a ingorer par CVSGravatar filliatr2000-11-08
* tous les binaires maintenant dans le repertoire binGravatar filliatr2000-11-08
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Bug sur précédent commitGravatar herbelin2000-11-07
* Nettoyage Names suiteGravatar herbelin2000-11-07
* MAJGravatar herbelin2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* Correction sur commit errone de la version 1.3Gravatar herbelin2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* OrthographeGravatar herbelin2000-11-07
* MAJGravatar herbelin2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* print_idl inlinéGravatar herbelin2000-11-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:47:36 +0000