coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Better implementation of summary unfreezing.	Pierre-Marie Pédrot	2013-11-24
*	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-22
*	Partial application hunt.	ppedrot	2013-11-07
*	Partial application in Globnames.	ppedrot	2013-11-06
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Native compiler: library compilation errors are now non fatal.	mdenes	2013-10-28
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	CList.prefix_of and CList.drop_prefix with a parametric equality	letouzey	2013-10-23
*	Removing some generic equalities.	ppedrot	2013-10-22
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	Summary: if an unfreeze function fails, print an error message	gareuselesinge	2013-10-18
*	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
*	Minimal implementation of `Shallow marshalling of Lib	gareuselesinge	2013-09-12
*	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-30
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	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-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	abstract+Defined: create opaque sub proofs (as pre-ParalITP)	gareuselesinge	2013-08-19
*	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-08
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	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-17
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09
*	Cosmetic change	gareuselesinge	2013-05-09
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Summary: support selective freeze	gareuselesinge	2013-05-06
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	coqtop -compile: avoid with_heavy_rollback when non-interactive	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Declaremods: some more minor cleanup	letouzey	2013-04-22
*	Minor simplifications in Declaremods and Safe_typing	letouzey	2013-04-15
*	Declaremods: drop some useless stuff (slight gain in vo size)	letouzey	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02