aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Expand)AuthorAge
* tests automatiquesGravatar herbelin2000-12-09
* Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...Gravatar herbelin2000-12-06
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Changement de la syntaxe des options -I et -RGravatar herbelin2000-11-30
* Ajout d'une option d'alias à -IGravatar herbelin2000-11-29
* Added -R inclusion to fix compilation in not-local configuration.Gravatar sacerdot2000-11-28
* -I inutiles pour coqc et utilisation de -R theories (pour garder trace des no...Gravatar herbelin2000-11-28
* Rajout de PolyListSyntax aussi dans MakefileGravatar herbelin2000-11-28
* Xml contrib retachedGravatar sacerdot2000-11-27
* Ajout BEST partout a coqcGravatar filliatr2000-11-24
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
* Ajout du clean pour tolink.mlGravatar delahaye2000-11-21
* ln -sf au lieu de ln -sGravatar filliatr2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
* XML débranchéGravatar filliatr2000-11-21
* Prise en compte camlp4.opt dans la configuration et le MakefileGravatar herbelin2000-11-20
* Prise en compte camlp4.opt dans la configuration et le MakefileGravatar herbelin2000-11-11
* -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
* nouveau load pathGravatar filliatr2000-11-08
* tous les binaires maintenant dans le repertoire binGravatar filliatr2000-11-08
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...Gravatar herbelin2000-11-05
* Few OCaml files in contrib/xmlGravatar sacerdot2000-11-03
* compilation avec make de Solaris; README et INSTALLGravatar filliatr2000-11-03
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* Ajouts pour les tactiques utilisateurGravatar delahaye2000-10-30
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
* ntrefiner.ml* removed in module xmlGravatar sacerdot2000-10-26
* xml contribution added to the MakefileGravatar sacerdot2000-10-25
* MAJGravatar herbelin2000-10-18
* mise a jour dependancesGravatar filliatr2000-09-18
* Suppression Redinfo Sosub AbstractionGravatar herbelin2000-09-14
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Pattern -> parsingGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* Adaptation pour Alpha.Gravatar delahaye2000-07-05
* Adaptation pour alpha.Gravatar delahaye2000-07-05
* Utilisation du STRIP de config/Makefile pour gérer le mode profileGravatar herbelin2000-06-29
* portage EAuto et RingGravatar filliatr2000-06-21
* dependance des CONTRIBVO envers initial.coqGravatar filliatr2000-06-12
* Changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:16:07 +0000