coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Fixing order of hypothesis in goal hypotheses compaction for coqtop.	Hugo Herbelin	2014-10-24
*	Fixing order of declarations in the function which compacts variables	Hugo Herbelin	2014-10-23
*	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin	2014-10-22
*	Fixing a (new) part of bug #2729.	Hugo Herbelin	2014-10-20
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Use smart mapping in map_constr_with_binders_left_to_right.	Matthieu Sozeau	2014-09-19
*	Moved code for finding subterms (pattern, induction, set, generalize, ...)	Hugo Herbelin	2014-06-28
*	Extra check for indirect dependency when abstracting a term which is	Hugo Herbelin	2014-06-28
*	Made the subterm finding function make_abstraction independent of the	Hugo Herbelin	2014-06-28
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fix a second, trickier, typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	Fix a small typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	remoteCounter: backup/restore	Enrico Tassi	2014-02-26
*	app_node, stack, state printers	Pierre Boutillier	2014-02-24
*	Partial application hunt.	ppedrot	2013-11-07
*	Closure optimizations.	ppedrot	2013-10-27
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Removing some generic equalities.	ppedrot	2013-10-22
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Removed some FIXME related to equality on universes.	ppedrot	2012-11-26
*	Small cleaning of interface in Univ	ppedrot	2012-11-26
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	More cleaning in CArray...	ppedrot	2012-09-18