aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Expand)Author
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-01-24Correction bug #1333 (test non récursivité des dépendances en d'autresherbelin
2006-11-06Changement du magic numbernotin
2006-09-12Indentation + svnpropnotin
2006-07-13Nombre magique pour la 8.1betaherbelin
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-26Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-11-01Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2005-02-05Localisation des libraries compilées uniquement via la structure du loadpath...herbelin
2004-11-17Bug 'Locate Library lib' quand 'lib' est aussi un moduleherbelin
2004-07-16Nouvelle en-têteherbelin
2004-04-14MAJ numéro magiqueherbelin
2004-03-30The XML exportation hook for require is now active for:sacerdot
2004-03-29Crocret xml pour Requireherbelin
2004-03-15preparation packages V8.0-cdrombarras
2004-01-28Bug de Require multipleherbelin
2003-12-23Changement numero magique; message d'erreur en cas de mauvaise syntaxeherbelin
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-05-19but Require dans une Sectionfilliatr
2003-05-15table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...filliatr
2003-02-03release 7.4; changement magic numberfilliatr
2003-01-09Export M + Module M <: SIGcoq
2002-12-19Petit netoyage dans libcoq
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
2002-10-12Forcer la réouverture d'un fichier explicitement requis même si leherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-15MAJ V7.3herbelin
2002-01-24Correction de l'ordre des open (sachant que de toutes façons, unherbelin
2002-01-18Pas d'assert false dans un try with !herbelin
2002-01-18Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...herbelin
2002-01-07Suppression de la dépendance des .vo en le nom physique des modulesherbelin
2001-12-19MAJ nombre magiqueherbelin
2001-12-17probleme des Require dans les sectionsbarras
2001-12-13compat ocaml 3.03filliatr
2001-12-05Rustine pour garder la compatibilité avec la 7.1 pour l'ordre des imports sa...herbelin
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-09-24One more boolean test bugherbelin
2001-09-24Bug test booléenherbelin
2001-09-20Nombre magique pour la V7.1herbelin
2001-09-20Pas de warning pour le -I . par défaut de Coqherbelin
2001-09-20warning silencieuxfilliatr
2001-09-20Restriction de l'avertissement add_loadpath au mode verbeuxherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 13:46:41 +0000