coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Fixes around typeclasses:	msozeau	2009-10-27
*	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau	2009-10-15
*	Correctly do backtracking during type class resolution even if only new	msozeau	2009-10-05
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Better use of transparency information for local hypotheses:	msozeau	2009-09-22
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	Fix "unsatisfiable constraints" error messages to include all the	msozeau	2009-06-18
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	When typing a non-dependent arrow, do not put the (anonymous) variable	msozeau	2009-06-11
*	Do a fixpoint on the result of typeclass search to force the	msozeau	2009-06-08
*	Minor unification changes:	msozeau	2009-05-18
*	Minor fixes in typeclasses:	msozeau	2009-05-16
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	Improvements in typeclasses eauto and generalized rewriting:	msozeau	2009-05-05
*	Fixes for bugs in r12110:	msozeau	2009-04-28
*	Cleanup old eauto code.	msozeau	2009-04-27
*	- Implementation of a new typeclasses eauto procedure based on success	msozeau	2009-04-27
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Move setoid_rewrite to its own module and do some clean up in	msozeau	2009-04-07
*	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin	2009-03-16
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	pushed evar reduction in kernel	barras	2009-02-06
*	Fix bug #2004 due to bad handling of evars in the unification for	msozeau	2009-01-21
*	Various little fixes:	msozeau	2009-01-18
*	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau	2009-01-12
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau	2008-12-14
*	Do not catch _all_ exceptions in setoid unification.	msozeau	2008-12-04
*	Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not	msozeau	2008-11-10
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau	2008-11-05
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Fixed bug #1966, wrong handling of evars.	msozeau	2008-10-18
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	Partial fix for bug #1948: recompute order of dependencies between	msozeau	2008-09-25
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau	2008-09-14
*	Fix bug #1939: defined evars were not substituted in some typeclasses	msozeau	2008-09-14
*	Remove redefinition of id in Program.Basics, just add maximal implicits.	msozeau	2008-09-13
*	Add a type argument to letin_tac instead of using casts and recomputing	msozeau	2008-09-12
*	Fix a bug reintroduced in [setoid_reflexivity] etc...	msozeau	2008-09-09
*	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau	2008-09-07