coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Implement the substitution function for global options. Fixes anomaly in ssre...	msozeau	2012-02-23
*	sequel of previous commit	letouzey	2011-12-21
*	Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...	letouzey	2011-12-21
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Proof using ...	gareuselesinge	2011-12-12
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Added a function to inspect current option state.	ppedrot	2011-11-24
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Adding the type infrastructure to handle properly API management of options	ppedrot	2011-11-18
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Heads: avoid potentially uncaught Not_found via an assert false	letouzey	2011-10-24
*	Temporary revert commit 14550 since it breaks a few contribs	letouzey	2011-10-12
*	in heads.ml, at least turn the Not_found of #2608 into assert false	letouzey	2011-10-11
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin	2011-10-08
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin	2011-09-24
*	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey	2011-09-22
*	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey	2011-09-15
*	Coqide: new backtracking code, based on the Backtrack command	letouzey	2011-09-05
*	Lib: remove strange code about backtracking to the current state	letouzey	2011-09-05
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Heads: generic equality on constr replaced by destructor	puech	2011-07-29
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Annotations at functor applications:	letouzey	2011-02-11
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Fix some typos	glondu	2011-01-11
*	Minor code improvements around libobject	herbelin	2010-10-31
*	Export definition of type implicits_list for contribs + fixed a	herbelin	2010-10-05
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Dead code in impargs (afaics, no more need, since r11242, to merge	herbelin	2010-10-03