aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
Commit message (Expand)AuthorAge
* 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
* Backtrack sur le warning Require en Section: trop contraignantGravatar herbelin2001-07-09
* Avertissement contre les Require dans le corps d'une sectionGravatar herbelin2001-07-05
* quelques bug reports mineursGravatar barras2001-05-07
* entetesGravatar filliatr2001-03-15
* protection contre certaines exceptions levees par marshal_{in,out}Gravatar barras2001-03-09
* on gele apres un Require => meilleures performances memoire, en particulier p...Gravatar filliatr2001-03-06
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
* Import module force l'ouverture du module même s'il était déjà ouvert afi...Gravatar herbelin2000-12-20
* Réparation de bugs de LoadPathGravatar herbelin2000-12-15
* load_path_entry structure simplified; field relative_subdir renamed to coq_dirpaGravatar sacerdot2000-11-29
* Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...Gravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28