coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Undo 12432 which caused an exponential behavior at Requires. Compilation time...	puech	2009-10-30
*	Fix incorrect registration of objects in libtypes.ml when defining a module.	puech	2009-10-28
*	Same as commit 12430 but with the good version of the function iter_all_segment	soubiran	2009-10-28
*	From now SearchAbout requests search also inside INCLUDE libobject.	soubiran	2009-10-28
*	Local/Global revision 12418 continued	herbelin	2009-10-26
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran	2009-10-23
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Fixed a bug introduced in revision 12265.	herbelin	2009-10-08
*	Relaxed error severity when encountering unknown library objects or tactic	gmelquio	2009-10-06
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix typos in comments	glondu	2009-09-17
*	Backtrack on the forced discharge of type class variables introduced	msozeau	2009-09-14
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Correction bug 2140.	soubiran	2009-08-27
*	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack	2009-08-14
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin	2009-08-07
*	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin	2009-08-06
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Support for binding Coq root read-only in -R option	herbelin	2009-07-01
*	propagation sur le trunk du commit 12101	soubiran	2009-06-26
*	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau	2009-06-26
*	Prevent automatic inference of implicit arguments when the auto flag is	msozeau	2009-06-01
*	Fix extract hyps to correctly discharge all hyps as described by keep	msozeau	2009-05-29
*	Fix implicit args code so that declarations are added for all	msozeau	2009-05-27
*	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau	2009-05-27
*	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin	2009-04-24
*	Fix premature optimisation in dependent induction: even variable args need	msozeau	2009-04-10
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	correction bug 2085	soubiran	2009-04-06
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Bug 2050, commit v8.2 11923-11924 ---> trunk	soubiran	2009-02-13
*	Correction bug coqdev Hermann lehener.	soubiran	2009-02-10
*	pushed evar reduction in kernel	barras	2009-02-06
*	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey	2009-02-03
*	Correction bug 2037.	soubiran	2009-01-30
*	Petit nettoyage faisant suite au commit #11847 .	aspiwack	2009-01-23
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	Uniformisation of some error messages + added test on setoid rewrite.	herbelin	2009-01-07
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01