coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Getting rid of Compat in the checker.	ppedrot	2012-10-04
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot	2012-09-26
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Made Pp.std_ppcmds opaque.	ppedrot	2012-09-13
*	Updating headers.	herbelin	2012-08-08
*	Fixing camlp4 compilation w.r.t previous commit	ppedrot	2012-06-22
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Flushing formatters before program exit.	ppedrot	2012-06-02
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Adapt the checker after commit 15080	letouzey	2012-03-26
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Noise for nothing	pboutill	2012-03-02
*	Add support for XDG_DATA_HOME and XDG_DATA_DIRS.	pboutill	2011-11-20
*	Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)	letouzey	2011-10-26
*	More descriptive error messages in checker	glondu	2011-10-20
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	bug 2423: consider "" as the empty prefix	barras	2011-07-07
*	fixed coqchk usage and man page + added option -coqlib	barras	2011-07-07
*	ported r14149 from v8.3 branch: bug in checker (redefined global)	barras	2011-05-23
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	Reorder search path order, so the standard library is search last.	herbelin	2011-04-14
*	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey	2011-04-12
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	checker: cleanup	glondu	2011-03-04
*	checker: add eta-expansion	glondu	2011-03-04
*	Propagate recent kernel changes to the checker	letouzey	2011-03-03
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Checker: remove some dead code	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Explicit Mod_checking signature	glondu	2010-09-16
*	Sharing is not anymore broken by traverse_module.	soubiran	2010-09-15
*	Fix likely semantic typos	glondu	2010-09-15
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	* checker/Safe_typing.LightenLibrary:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27