aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
Commit message (Expand)AuthorAge
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Suite de la révision #11212Gravatar notin2008-07-08
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* Crocret xml pour RequireGravatar herbelin2004-03-29
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* *** empty log message ***Gravatar barras2003-03-12
* Petit netoyage dans libGravatar coq2002-12-19
* 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
* Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...Gravatar herbelin2002-01-18
* ParsingGravatar herbelin2001-08-10
* entetesGravatar filliatr2001-03-15
* 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
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...Gravatar herbelin2000-11-29