coq - the Coq proof assistant

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