coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	obligations: wrap Ephemeron.get to make error more informative	Enrico Tassi	2015-06-23
*	Wrap the program_info type up in the ephemeron mechanism	Alec Faithfull	2015-06-23
*	Program: Do not reduce obligation types preemptively, only at	Matthieu Sozeau	2015-04-13
*	Add the possibility of defining opaque terms with program.	mlasson	2015-01-21
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Exporting the function handling side-effects only applied to terms.	Pierre-Marie Pédrot	2014-11-20
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	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
*	Fix program using an the unsubstituted type of the original obligation	Matthieu Sozeau	2014-08-14
*	- Fix bug introduced in obligations which wouldn't consider all evars that are	Matthieu Sozeau	2014-07-16
*	Better handling of the universe context in case of Admitted proof obligations.	Matthieu Sozeau	2014-07-10
*	When defining a monomorphic Program, do not allow arbitrary instantiations	Matthieu Sozeau	2014-07-03
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Safer entry point of primitive projections in the kernel, now it does recognize	Matthieu Sozeau	2014-06-17
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau	2014-06-04
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	- 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
*	- Rename eq to equal in Univ, document new modules, set interfaces.	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
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Add an option to shrink the context of program obligations to avoid	msozeau	2013-06-06
*	Getting rid of LtacLocated exception transformer.	ppedrot	2013-05-28
*	Merging Context and Sign.	ppedrot	2013-04-29