coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Turn evars created by a tactic application into a subgoal immediately in	msozeau	2009-12-06
*	Fix anomaly when using typeclass resolution with filtered hyps in evars.	msozeau	2009-12-06
*	Restored rewriting of JMeq using JMeq_rect and co when the domains are the same	herbelin	2009-12-03
*	Fix make_exact_entry to allow applying [forall x, P x] hints directly,	msozeau	2009-12-01
*	Fix bug in typeclass resolution. Better handling of universes in	msozeau	2009-12-01
*	Fix backtracking heuristic in typeclass resolution.	msozeau	2009-11-30
*	Substitute terms for evars-as-goals as soon as they are solved in	msozeau	2009-11-27
*	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau	2009-11-24
*	Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...	puech	2009-11-21
*	Addendum to revision 12501.	herbelin	2009-11-12
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Backtracking on the use of automatically generated schemes for	herbelin	2009-11-11
*	Compatibility ocaml <= 3.09	herbelin	2009-11-10
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Quick fix for restoring a left-to-right rewriting lemma compatible	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	- Fix discharge bug in typeclasses: some constrs were not actually	msozeau	2009-11-06
*	Misc fixes.	msozeau	2009-11-06
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Clarification in comments	glondu	2009-10-28
*	Remove old compatibility stuff (Tacred.nf)	glondu	2009-10-28
*	Make usage of Dyn explicit	glondu	2009-10-28
*	Backport fix for indexing of sorts which collapse every Type occurrence	msozeau	2009-10-28
*	Fixes around typeclasses:	msozeau	2009-10-27
*	fix previous commit	corbinea	2009-10-27
*	fixed czar bug with parametric inductives	corbinea	2009-10-27
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin	2009-10-25
*	Add support for remaining side-conditions in "apply in as".	herbelin	2009-10-25
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin	2009-10-24
*	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
*	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau	2009-10-15
*	Relaxed error severity when encountering unknown library objects or tactic	gmelquio	2009-10-06
*	Correctly do backtracking during type class resolution even if only new	msozeau	2009-10-05
*	Changed the way to support compatibility with previous versions.	herbelin	2009-10-04
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Added option "Unset Dependent Propositions Elimination" to protect	herbelin	2009-10-03
*	Remove legacy export_* functions	glondu	2009-09-29
*	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin	2009-09-27
*	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Better use of transparency information for local hypotheses:	msozeau	2009-09-22
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	- Fixed a bug in checking that implicit arguments are all correctly	herbelin	2009-09-18
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17