aboutsummaryrefslogtreecommitdiff
path: root/library/library.mli
AgeCommit message (Expand)Author
2016-05-19coqc: support -o option to specify output file nameEnrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25The -compile option now accepts ".v" files and outputs a warning otherwise.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-05-12Use the Hook module here and there.ppedrot
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-04-12lib directory is cut in 2 cma.pboutill
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-07-08Suite de la révision #11212notin
2008-07-07Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...notin
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2004-07-16Nouvelle en-têteherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 10:00:22 +0000