aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Expand)Author
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
2001-09-19Autorisation de surcharge d'un -R par un -Iherbelin
2001-09-19Typoherbelin
2001-09-18Tentative de canonisation des répertoires physiquesherbelin
2001-09-18Quelques heuristiques pour gérer des représentations similaires de paths sy...herbelin
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
2001-08-10Parsingherbelin
2001-07-09Backtrack sur le warning Require en Section: trop contraignantherbelin
2001-07-05Avertissement contre les Require dans le corps d'une sectionherbelin
2001-05-07quelques bug reports mineursbarras
2001-03-15entetesfilliatr
2001-03-09protection contre certaines exceptions levees par marshal_{in,out}barras
2001-03-06on gele apres un Require => meilleures performances memoire, en particulier p...filliatr