coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: module_kind to Declaremods	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias	2018-04-06
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	LtacProf for Coq trunk	Jason Gross	2016-06-05
*	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
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
*	Update headers.	Maxime Dénès	2015-01-12
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	- 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
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Minor simplifications in Declaremods and Safe_typing	letouzey	2013-04-15
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	Dir_path --> DirPath	letouzey	2013-02-19
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	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
*	Noise for nothing	pboutill	2012-03-02
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	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
*	Variant !F M for functor application that does not honor the Inline declarations	letouzey	2010-01-17
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey	2009-12-07
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey	2009-11-16
*	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey	2009-11-16