aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Expand)Author
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-08-27* library/Library: Reformulate a comment.regisgia
2010-08-27* library/Library: Document.regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-08-27* Improve documentation of LightenLibrary.regisgia
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
2010-08-27* library/Library: Remove the use of the old-fashioned lighten_library.regisgia
2010-08-27* library/Library: Remove lighten_library definition.regisgia
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2009-02-06pushed evar reduction in kernelbarras
2009-01-18Backporting from v8.2 to trunk:herbelin
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-11-25correction bug 1997.soubiran
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
2008-07-24moved magic numbers to configure (share coq/coqchk)barras
2008-07-08Suite de la révision #11212notin
2008-06-30Fichiers oubliés lors du 11188 :-(herbelin
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-12Confusion sur commit précédent de library. La capture du Not_foundherbelin
2008-06-11Bug dans l'adaptation de library_full_filename lors du débranchementherbelin
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 12:06:05 +0000