aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
Commit message (Expand)AuthorAge
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Remove Library.mem, which is pointless since 8.5.Gravatar Guillaume Melquiond2015-12-31
|/
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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