coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Forbid Require inside interactive modules and module types.	Maxime Dénès	2014-12-25
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	Fix Declaremods.end_library (Closes: #3536)	Enrico Tassi	2014-09-02
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	STM: make -async-proofs on work from coqc too	Enrico Tassi	2014-03-18
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Modops.destr_functor without useless env	letouzey	2013-07-17
*	Lib.contents () instead of Lib.contents_after None	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Declaremods: some more minor cleanup	letouzey	2013-04-22
*	Minor simplifications in Declaremods and Safe_typing	letouzey	2013-04-15
*	Declaremods: drop some useless stuff (slight gain in vo size)	letouzey	2013-04-15
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Declaremods: a few syntactic improvements	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	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 Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Monomorphization (library)	ppedrot	2012-11-22
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey	2011-09-15
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Annotations at functor applications:	letouzey	2011-02-11