aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
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
2003-06-15Ground major update ... mmm, sounds exciting !corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14dependcoq integre les fichiers de fsetsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4165 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4158 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground update, new files.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13install-fsetsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4151 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13FSets, mais pas compile' par make worldfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Module Bij inutiliseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4129 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-02 au lieu de makemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4095 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23coqide: blaster 2monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4071 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-23fabrication de ide/utf8.voletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4070 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22coqide: blaster V1monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructutation Hipattern Patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4034 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19configure et make install s'occupent de CoqIde tout seulsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14coqide: .* on start/add \n on eofmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14coqide: load/save file encoding support/monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07entréé translation2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3990 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Ajout ChoiceFactsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3977 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28coqide: search forwardmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3969 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28fichier de pref coq IDE en ASCII (ENFIN)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3963 85f007b7-540e-0410-9357-904b9bb8a0f7