coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Christmas is over...	Maxime Dénès	2014-01-15
*	.vi files: .vo files without proofs	Enrico Tassi	2014-01-04
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	inductive.ml : get rid of some obvious (Lazy.force (lazy t))	letouzey	2013-10-24
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Get rid of polymorphic equality in "checker/subtyping.ml".	xclerc	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
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	Ephemeron: marshaling friendly keys	gareuselesinge	2013-10-18
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Adding dynamic value printing to votour through a registering mechanism.	ppedrot	2013-08-23
*	Misc changes around coqtop.ml :	letouzey	2013-08-22
*	Change in vo format : digest aren't Marshalled anymore	letouzey	2013-08-22
*	Fixing votour	ppedrot	2013-08-20
*	Fix compilation of coqcheck	gareuselesinge	2013-08-20
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Repair coqcheck : constant_body constraints are also future	letouzey	2013-08-20
*	checker validation fixed w.r.t. Futures	gareuselesinge	2013-08-09
*	checker validation made a bit more verbose	gareuselesinge	2013-08-09
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Added a generic notion of hook. Hooks are functions to be set	ppedrot	2013-05-12
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Remove deprecated option -no-hash-consing (currently doing nothing)	letouzey	2013-04-23
*	Checker: vo validation checks the absence of Var/Evar/Meta	letouzey	2013-04-15
*	Checker : a md5-based way to ensure checker/values.ml is always in sync	letouzey	2013-04-15
*	votour: a small tool for guided tours of .vo	letouzey	2013-04-15
*	Checker: vo validation is now done in check.ml (and always)	letouzey	2013-04-15
*	Checker: get rid of code handling section variables	letouzey	2013-04-15
*	Checker: empty sections hardcoded in cb and mind	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Mod_subst.force: avoid using join when only one subst	letouzey	2013-04-02
*	Minor cleanup concerning Mod_subst.MBImap	letouzey	2013-04-02
*	Safe_typing+Libary: use some arrays instead of lists in vo structures	letouzey	2013-03-28
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Removing mandatory suffixes for library files.	ppedrot	2013-03-21
*	Checker: simplify a bit its exception handler	letouzey	2013-03-17
*	Fix compilation of coqchk (broken by commit 16268), bis repetita	letouzey	2013-03-13
*	Fix compilation of coqchk (broken by commit 16268)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 2)	letouzey	2013-03-12
*	Restrict (try...with...) to avoid catching critical exn (part 1)	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Names: Modularize constant and mutual_inductive	letouzey	2013-02-26