coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-01	Fix handling of instance declarations in presence of let-ins (bug	msozeau
2009-12-30	Fixing bug #2193: computation of dependencies in the "match" return	herbelin
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-22	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-21	In "progress", extending the set of evars w/o solving an existing one is	herbelin
2009-12-14	Improved strategy for rewriting lemma possibly depending because of evars.	herbelin
2009-12-03	Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)	herbelin
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-15	Fix type class discharge again.	msozeau
2009-11-12	Backtrack on fixing #2167	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Redoing broken commit r12498 (fixing bug #2167 + attempt to test the	herbelin
2009-11-11	Fixing bug #2167 + attempt to test the compatibility of a more robust	herbelin
2009-11-09	Commit 12485 continued.	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-08	Took local definitions into account in the test for deciding whether	herbelin
2009-11-06	- Fix discharge bug in typeclasses: some constrs were not actually	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-11-02	Reverted an incorrect code simplification in function status_changed	herbelin
2009-10-30	Attempt to capture on time unification errors for "with" bindings.	herbelin
2009-10-30	Take constraints into account in the "instantiate" tactic	herbelin
2009-10-29	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-10-28	Make usage of Dyn explicit	glondu
2009-10-27	Fixes around typeclasses:	msozeau
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-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	herbelin
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-08-23	A new kind of automatically generated scheme "congr" for equality types	herbelin
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-13	Made unification patch 12268 even more ad hoc (if evars remain in a	herbelin
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	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-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau