coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-23	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-08	Fixed a bug introduced in revision 12265.	herbelin
2009-10-06	Relaxed error severity when encountering unknown library objects or tactic	gmelquio
2009-09-17	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-14	Backtrack on the forced discharge of type class variables introduced	msozeau
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-27	Correction bug 2140.	soubiran
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	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-02	Improved parameterization of Coq:	herbelin
2009-07-01	Support for binding Coq root read-only in -R option	herbelin
2009-06-26	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-01	Prevent automatic inference of implicit arguments when the auto flag is	msozeau
2009-05-29	Fix extract hyps to correctly discharge all hyps as described by keep	msozeau
2009-05-27	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-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-04-10	Fix premature optimisation in dependent induction: even variable args need	msozeau
2009-04-08	Some dead code removal + cleanups	letouzey
2009-04-06	correction bug 2085	soubiran
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-02-13	Bug 2050, commit v8.2 11923-11924 ---> trunk	soubiran
2009-02-10	Correction bug coqdev Hermann lehener.	soubiran
2009-02-06	pushed evar reduction in kernel	barras
2009-02-03	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey
2009-01-30	Correction bug 2037.	soubiran
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-17	DISCLAIMER	puech
2009-01-07	Uniformisation of some error messages + added test on setoid rewrite.	herbelin
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-18	Correction d'un bug causant un Not_found dans la contrib FSet.	soubiran
2008-11-25	correction bug 1997.	soubiran
2008-11-23	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-10-28	Correction bug 1979.	soubiran
2008-10-21	Correction bug #1969.	soubiran
2008-10-15	Report des commits 11417 et 11437 de la v8.2	soubiran