aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2004-03-29"xml" target removed from generated makefiles (since it was no longer used)sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5602 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29MAJkirchner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5601 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout option raw-comments pour supprimer affichage de <table>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5580 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout option raw-comments pour supprimer affichage de <table>; typosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5579 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26MAJ mot-clesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5578 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Bug <BR>; ajout option raw_comment pas d'affichage de <table>; MAJ mot-clesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5577 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17suppression du ./ devant (et .\ sous Windows)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5522 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16application patch de Lionel Elie Mamane pour option -R et chemins ↵filliatr
relatifs/absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5504 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15identification ./f et f dans coqdep -sortfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5483 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15Parametersfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5482 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01ocaml 3.07 -> 3.06filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5402 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5389 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-25indexation Record / bug gallina sur := en V8filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5382 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5378 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-24coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5377 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- 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
2003-12-12option -n de coq-texmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5090 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-11Nouvelle version qui compile dans un sous-repertoire avant d'ecraser le ↵herbelin
repertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5087 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10MAJ OTHERFLAGSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4854 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Ajout option -impredicative-setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Passage options via COQFLAGS plutot que OPTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4472 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Outil de test de la traduction et de la compilation en v8 sans modification desherbelin
sources git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4393 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Message pour les erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4382 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10typonarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4343 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-05affichage de la nature des colonnesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4304 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-12Bug et amliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Outils de traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4252 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-02rm -f .depend (sans le -f "make depend" echoue lorsque le .dependfilliatr
n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4213 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Modif de coq-tex - meilleur affichage des suite de coq_example'scoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4003 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24on sait se refaire uniquement si option -ffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3697 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-24coq_makefile dit comment faire le .depend (evite l'echec lorsquefilliatr
.depend n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14prise en compte des sous-repertoires Coq de maniere dynamiquefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3682 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04mdule --> modulemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3374 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04fichiers DOSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3371 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15Bug de coqdep qui n'acceptait pas les fichiers DOS (cf Binome.v)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3243 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3236 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15commit du calcul des dependances un peu plus robustebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-10gestion coherente de l'option -R et des Require A.B.C.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3112 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01backslahs foireuxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3059 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Filtrage redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-16Un peu plus de flexibilité pour la position du '.' finalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3010 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-18coq_makefile utilise maintenant coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2793 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-30Ajout des -I contribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2738 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-15coq-inferior, by Marco Maggesifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2644 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04meilleure gestion du point terminalfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2611 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:03:16 +0000