coq - The formal proof system

Age	Commit message (Expand)	Author
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	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-02-28	Fix output test-suite 'simpl tactic' -> 'reduction tactics'	Pierre Boutillier
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
2014-02-26	New compilation mode -vi2vo	Enrico Tassi
2014-02-24	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-09-19	Prettyp: avoid useless "let module"	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-08-08	State Transaction Machine	gareuselesinge
2013-08-01	Added printing of instance priority to the Print Instances command.	ppedrot
2013-07-17	Lib.contents () instead of Lib.contents_after None	letouzey
2013-05-05	Now printing body of abbreviations (i.e. notation with a name) with	herbelin
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey
2013-03-05	More monomorphization.	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-21	Print univ constraints generated by a constant or inductive (when flag is set)	barras
2012-11-13	Added a CString module.	ppedrot
2012-09-14	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-08-08	Updating headers.	herbelin
2012-07-20	Fixing test-suite	pboutill
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-12	Fixing test-suite after last storm in Pp.	pboutill
2012-05-29	place all pretty-printing files in new dir printing/	letouzey