coq - The formal proof system

Age	Commit message (Expand)	Author
2014-02-03	Allocation-friendly mapping functions in Nametab.	Pierre-Marie Pédrot
2014-01-05	STM: modules do not prevent proofs from being ASync	Enrico Tassi
2014-01-05	coqtop: -check-vi-tasks and -schedule-vi-checking	Enrico Tassi
2014-01-04	.vi files: .vo files without proofs	Enrico Tassi
2013-12-24	Qed: feedback when type checking is done	Enrico Tassi
2013-12-12	Patch for supporting [From Xxx Require Yyy Zzz.]	Gregory Malecha
2013-12-02	Print logical name rather than path (thus allowing reproducible tests).	xclerc
2013-11-24	Better implementation of summary unfreezing.	Pierre-Marie Pédrot
2013-11-22	Using hashes in Summary, like the previous commit did with Dyn.	Pierre-Marie Pédrot
2013-11-22	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot
2013-11-07	Partial application hunt.	ppedrot
2013-11-06	Partial application in Globnames.	ppedrot
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-28	Native compiler: library compilation errors are now non fatal.	mdenes
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	CList.prefix_of and CList.drop_prefix with a parametric equality	letouzey
2013-10-22	Removing some generic equalities.	ppedrot
2013-10-18	Future: ported to Ephemeron + exception enhancing	gareuselesinge
2013-10-18	Summary: if an unfreeze function fails, print an error message	gareuselesinge
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-12	Minimal implementation of `Shallow marshalling of Lib	gareuselesinge
2013-08-30	summary for ML modules made correct	gareuselesinge
2013-08-30	ind_tables: properly handling side effects	gareuselesinge
2013-08-30	recdef: restore old semantics (pre STM)	gareuselesinge
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-22	Change in vo format : digest aren't Marshalled anymore	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-08-20	Safe_typing code refactoring	letouzey
2013-08-19	abstract+Defined: create opaque sub proofs (as pre-ParalITP)	gareuselesinge
2013-08-08	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge
2013-08-08	Simple machinery to detect EXTEND that interpret during parsing	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-08-04	Removing useless casts between arrays and lists.	ppedrot
2013-07-17	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-10	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes
2013-05-12	Use the Hook module here and there.	ppedrot
2013-05-09	Use definition_entry to declare local definitions	gareuselesinge
2013-05-09	Cosmetic change	gareuselesinge
2013-05-08	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-05-06	Summary: support selective freeze	gareuselesinge
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot