aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Collapse)AuthorAge
* preparation a la release 8.0Gravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5655 85f007b7-540e-0410-9357-904b9bb8a0f7
* tools/coq_vo2xml removed since no longer in use.Gravatar sacerdot2004-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5603 85f007b7-540e-0410-9357-904b9bb8a0f7
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
| | | | | | | | On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained designed is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5562 85f007b7-540e-0410-9357-904b9bb8a0f7
* install de coqdocGravatar barras2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5523 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar coq2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5505 85f007b7-540e-0410-9357-904b9bb8a0f7
* install de pcoq incorrect + spec rpmGravatar barras2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5503 85f007b7-540e-0410-9357-904b9bb8a0f7
* pages de man pour coqwc et coqdocGravatar filliatr2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5502 85f007b7-540e-0410-9357-904b9bb8a0f7
* ROmegaGravatar mohring2004-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5430 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdocGravatar filliatr2004-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5379 85f007b7-540e-0410-9357-904b9bb8a0f7
* files from contrib/interface need files from contrib/field, the variableGravatar bertot2004-02-19
| | | | | | | LOCALINCLUDES needs to contain -I contrib/field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5362 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvaise dependance en states7/initial.coqGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5325 85f007b7-540e-0410-9357-904b9bb8a0f7
* clean-ide plus precisGravatar herbelin2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5293 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganize the order of librairies in the entry CMO to make sure this canGravatar bertot2004-02-02
| | | | | | | be used as a reference to know in which order the libraries should be loaded git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5278 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure separation de compil et install de coq, coqide et coq-interfaceGravatar barras2004-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction des cibles des theories indviduellesGravatar herbelin2004-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5255 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement des cma et cmxa dans les sous-repertoiresGravatar barras2004-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement lexer pour dependance dans constrinternGravatar herbelin2004-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5226 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide utf8Gravatar marche2004-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5222 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajoute une option -linkall dans compilation de bin/parser pour assurer queGravatar bertot2004-01-16
| | | | | | | les analyseurs syntaxiques sont bien charges git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5212 85f007b7-540e-0410-9357-904b9bb8a0f7
* make libraries, lexing of more utf8 symbolsGravatar marche2004-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de Rsyntax en v8Gravatar herbelin2004-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cible install-ideGravatar herbelin2004-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cible redondante qui trouble les make non linuxGravatar herbelin2004-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5182 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'installation ne copiait pas les .vo du traducteurGravatar herbelin2003-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5064 85f007b7-540e-0410-9357-904b9bb8a0f7
* installationGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et ↵Gravatar herbelin2003-11-29
| | | | | | 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
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵Gravatar herbelin2003-11-21
| | | | | | et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
* tout clean-ide dans cleanGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration ZArithGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements de syntaxeGravatar barras2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
* make moins verbeux, suite (et fin?)Gravatar letouzey2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Biblio standard sans mention de la possibilite d'etre impredicatif; ↵Gravatar herbelin2003-11-07
| | | | | | 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
* Ajout NArith et restructuration ZArithGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4802 85f007b7-540e-0410-9357-904b9bb8a0f7
* pour que make clean efface ide/utf8_convert.ml venant d'un .mllGravatar letouzey2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Diaconescu.vGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4773 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux fichiers dans Logic; prise en compte de l'option ↵Gravatar herbelin2003-10-28
| | | | | | -strongly-classical la compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout NArithRingGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update + Linear removalGravatar corbinea2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour eviter que newtheories/Lists/List.v soit refait quand PolyList.v est ↵Gravatar herbelin2003-10-15
| | | | | | 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
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à ↵Gravatar herbelin2003-10-10
| | | | | | 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
* Renommage en v8 de PolyList en List et List en MonoListGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage no-strict en -strict-implicitGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage no-strict en -strict-implicitGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4541 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour rendre make un peu moins verbeuxGravatar letouzey2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4532 85f007b7-540e-0410-9357-904b9bb8a0f7
* NEWCONTRIBVO doit apparaitre apres CONTRIBVOGravatar herbelin2003-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4531 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand ↵Gravatar herbelin2003-10-04
| | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 21:25:51 +0000