coq - The formal proof system

Age	Commit message (Expand)	Author
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2010-01-26	Quick fix for references to section variables unbound in the current	msozeau
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-19	Backtrack on making exact hints for lemmas starting with products	msozeau
2009-12-06	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-01	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-11-30	Fix backtracking heuristic in typeclass resolution.	msozeau
2009-11-27	Substitute terms for evars-as-goals as soon as they are solved in	msozeau
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-27	Fixes around typeclasses:	msozeau
2009-10-15	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
2009-10-04	Removal of trailing spaces.	serpyc
2009-09-22	Better use of transparency information for local hypotheses:	msozeau
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-11	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-08	Do a fixpoint on the result of typeclass search to force the	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-05-16	Minor fixes in typeclasses:	msozeau
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-05-05	Improvements in typeclasses eauto and generalized rewriting:	msozeau
2009-04-28	Fixes for bugs in r12110:	msozeau
2009-04-27	Cleanup old eauto code.	msozeau
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-08	Some dead code removal + cleanups	letouzey
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2009-01-21	Fix bug #2004 due to bad handling of evars in the unification for	msozeau
2009-01-18	Various little fixes:	msozeau
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau
2008-12-04	Do not catch _all_ exceptions in setoid unification.	msozeau
2008-11-10	Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau