coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-07	Reorder resolution of type class and unification constraints.	msozeau
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-02-22	Improve unification when evars and metas are mixed.	msozeau
2010-02-16	Compute the correct generalization information when discharging a class	msozeau
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-26	Quick fix for references to section variables unbound in the current	msozeau
2010-01-12	Removing some betaiota-redexes in error messages (an experiment)	herbelin
2010-01-12	Typo in error message	herbelin
2010-01-12	Added module sharing support for typeclasses and hints (pri_auto_tactic).	soubiran
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