aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
Commit message (Expand)AuthorAge
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...Gravatar herbelin2005-11-26
* Types inductifs parametriquesGravatar mohring2005-11-02
* Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...Gravatar herbelin2005-11-01
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Localisation des libraries compilées uniquement via la structure du loadpath...Gravatar herbelin2005-02-05
* Bug 'Locate Library lib' quand 'lib' est aussi un moduleGravatar herbelin2004-11-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* MAJ numéro magiqueGravatar herbelin2004-04-14
* The XML exportation hook for require is now active for:Gravatar sacerdot2004-03-30
* Crocret xml pour RequireGravatar herbelin2004-03-29
* preparation packages V8.0-cdromGravatar barras2004-03-15
* Bug de Require multipleGravatar herbelin2004-01-28
* Changement numero magique; message d'erreur en cas de mauvaise syntaxeGravatar herbelin2003-12-23
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* but Require dans une SectionGravatar filliatr2003-05-19
* table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...Gravatar filliatr2003-05-15
* release 7.4; changement magic numberGravatar filliatr2003-02-03
* Export M + Module M <: SIGGravatar coq2003-01-09
* Petit netoyage dans libGravatar coq2002-12-19
* Préservation de la cohérence du cache en cas d'erreur au chargementGravatar herbelin2002-10-29
* Forcer la réouverture d'un fichier explicitement requis même si leGravatar herbelin2002-10-12
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* MAJ V7.3Gravatar herbelin2002-05-15
* Correction de l'ordre des open (sachant que de toutes façons, unGravatar herbelin2002-01-24
* Pas d'assert false dans un try with !Gravatar herbelin2002-01-18
* Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...Gravatar herbelin2002-01-18
* Suppression de la dépendance des .vo en le nom physique des modulesGravatar herbelin2002-01-07
* MAJ nombre magiqueGravatar herbelin2001-12-19
* probleme des Require dans les sectionsGravatar barras2001-12-17
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Rustine pour garder la compatibilité avec la 7.1 pour l'ordre des imports sa...Gravatar herbelin2001-12-05
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* One more boolean test bugGravatar herbelin2001-09-24
* Bug test booléenGravatar herbelin2001-09-24
* Nombre magique pour la V7.1Gravatar herbelin2001-09-20
* Pas de warning pour le -I . par défaut de CoqGravatar herbelin2001-09-20
* warning silencieuxGravatar filliatr2001-09-20
* Restriction de l'avertissement add_loadpath au mode verbeuxGravatar herbelin2001-09-20
* Autorisation de surcharge d'un -R par un -IGravatar herbelin2001-09-19
* TypoGravatar herbelin2001-09-19
* Tentative de canonisation des répertoires physiquesGravatar herbelin2001-09-18
* Quelques heuristiques pour gérer des représentations similaires de paths sy...Gravatar herbelin2001-09-18
* Suppression des library roots, on teste si un nom est absolu autrementGravatar herbelin2001-09-07
* ParsingGravatar herbelin2001-08-10