coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	STM: simplify how the term part of a side effect is retrieved	Enrico Tassi	2014-10-13
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	- Do module substitution inside mind_record.	Matthieu Sozeau	2014-07-25
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Safer entry point of primitive projections in the kernel, now it does recognize	Matthieu Sozeau	2014-06-17
*	ind_tables: always declare side effects (Closes: HOTT#110)	Enrico Tassi	2014-06-08
*	Declare: fix Future management	Enrico Tassi	2014-05-16
*	- 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
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	ind_tables: properly handling side effects	gareuselesinge	2013-08-30
*	abstract+Defined: create opaque sub proofs (as pre-ParalITP)	gareuselesinge	2013-08-19
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Dir_path --> DirPath	letouzey	2013-02-19
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	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 Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (library)	ppedrot	2012-11-25
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Noise for nothing	pboutill	2012-03-02