aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Expand)Author
2004-02-19files from contrib/interface need files from contrib/field, the variablebertot
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-02-12Mauvaise dependance en states7/initial.coqherbelin
2004-02-04clean-ide plus precisherbelin
2004-02-02reorganize the order of librairies in the entry CMO to make sure this canbertot
2004-01-27meilleure separation de compil et install de coq, coqide et coq-interfacebarras
2004-01-27Correction des cibles des theories indviduellesherbelin
2004-01-26deplacement des cma et cmxa dans les sous-repertoiresbarras
2004-01-21Deplacement lexer pour dependance dans constrinternherbelin
2004-01-20coqide utf8marche
2004-01-16ajoute une option -linkall dans compilation de bin/parser pour assurer quebertot
2004-01-14make libraries, lexing of more utf8 symbolsmarche
2004-01-13Suppression de Rsyntax en v8herbelin
2004-01-08Ajout cible install-ideherbelin
2004-01-07Cible redondante qui trouble les make non linuxherbelin
2003-12-03L'installation ne copiait pas les .vo du traducteurherbelin
2003-11-29installationherbelin
2003-11-29Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7...herbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...herbelin
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-18tout clean-ide dans cleanherbelin
2003-11-12Restructuration ZArithherbelin
2003-11-12petits changements de syntaxebarras
2003-11-09make moins verbeux, suite (et fin?)letouzey
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatif; Hurkens_s...herbelin
2003-11-05Ajout NArith et restructuration ZArithherbelin
2003-11-04pour que make clean efface ide/utf8_convert.ml venant d'un .mllletouzey
2003-11-02Ajout Diaconescu.vherbelin
2003-10-28Nouveaux fichiers dans Logic; prise en compte de l'option -strongly-classical...herbelin
2003-10-22Ajout NArithRingherbelin
2003-10-16Ground update + Linear removalcorbinea
2003-10-15Pour eviter que newtheories/Lists/List.v soit refait quand PolyList.v est ref...herbelin
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-10Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à c...herbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-08Renommage no-strict en -strict-implicitherbelin
2003-10-08Renommage no-strict en -strict-implicitherbelin
2003-10-06Pour rendre make un peu moins verbeuxletouzey
2003-10-06NEWCONTRIBVO doit apparaitre apres CONTRIBVOherbelin
2003-10-04Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand new...herbelin
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
2003-10-03Bug cible newtheories/Init + diversherbelin
2003-10-03Nettoyage, simplification et compatibilite -jherbelin
2003-10-03oubli de deux flags -v7letouzey
2003-09-26pa_ifdef.cmo redondantherbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-22Passage à la V8 par défautherbelin
2003-09-15Reprise de coqbinaries dans translationherbelin
2003-09-13Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisieherbelin