coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Safe_typing+Libary: use some arrays instead of lists in vo structures	letouzey	2013-03-28
*	Synchronizing loadpath with the backtrack mechanism.	ppedrot	2013-03-26
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Removing mandatory suffixes for library files.	ppedrot	2013-03-21
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Declaremods: a few syntactic improvements	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 1)	letouzey	2013-03-12
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Mod_subst: misc reformulations	letouzey	2013-02-26
*	Reduced the noise level when dynlinking in bytecode mode or when	mdenes	2013-02-24
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19