aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
2004-01-14make libraries, lexing of more utf8 symbolsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Suppression de Rsyntax en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-08Ajout cible install-ideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5185 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-07Cible redondante qui trouble les make non linuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5182 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-03L'installation ne copiait pas les .vo du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5064 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29installationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5039 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et ↵herbelin
states7; Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5028 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵herbelin
et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18tout clean-ide dans cleanherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4942 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09make moins verbeux, suite (et fin?)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4844 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatif; ↵herbelin
Hurkens_set disparait de la biblio standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Ajout NArith et restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04pour que make clean efface ide/utf8_convert.ml venant d'un .mllletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4786 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Ajout Diaconescu.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4773 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Nouveaux fichiers dans Logic; prise en compte de l'option ↵herbelin
-strongly-classical la compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4728 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Ajout NArithRingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4703 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Ground update + Linear removalcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Pour eviter que newtheories/Lists/List.v soit refait quand PolyList.v est ↵herbelin
refait non parce qu'il faut mais parce qu'il a disparu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4640 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Death of 'a somewhat cryptic module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à ↵herbelin
cablage en dur de Inversion dans tacexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4564 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Renommage no-strict en -strict-implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4542 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Renommage no-strict en -strict-implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4541 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06Pour rendre make un peu moins verbeuxletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4532 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06NEWCONTRIBVO doit apparaitre apres CONTRIBVOherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4531 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand ↵herbelin
newtheories et newcontrib n'existent pas encore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4528 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4526 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Bug cible newtheories/Init + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4523 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Nettoyage, simplification et compatibilite -jherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4520 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03oubli de deux flags -v7letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4519 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26pa_ifdef.cmo redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4488 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵herbelin
TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-15Reprise de coqbinaries dans translationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4399 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-13Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4397 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Retour à des cibles plus explicites: world7 et world8, install7 et install8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4394 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout install7 et coqwc dans toolsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4392 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout cible world7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4391 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
choix du parseur en fonction de cette option Suppression DatatypesSyntax et PeanoSyntax qui était vides git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4388 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare et Impargs à la fin de interp pour que Declare ↵herbelin
accède à tout interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4366 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05install coqwcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4303 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05coqwcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4302 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Fusion -translate et -ftranslateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Option -v8 à coqtop lance coqtopnewherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4256 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-02suppression de newtautocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4214 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-24suppression de FSets (redevient une contrib)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 13:35:29 +0000