coq - The formal proof system

Age	Commit message (Expand)	Author
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2009-01-03	Fixed two problems:	herbelin
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-30	- Fixed bugs and compatibilities issues in	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-18	- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side	herbelin
2008-12-16	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau
2008-12-12	Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...	herbelin
2008-12-09	About "apply in":	herbelin
2008-12-04	Do not catch _all_ exceptions in setoid unification.	msozeau
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-23	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
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-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-07	Add the ability to give a specific tactic to solve each obligation in	msozeau
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-11-04	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin
2008-10-29	Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-25	More debugging of handling of open constrs with typeclasses:	msozeau
2008-10-23	Forgot one file which had other local modifications...	msozeau
2008-10-23	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-18	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-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-09-25	Various little improvements:	msozeau
2008-09-25	Partial fix for bug #1948: recompute order of dependencies between	msozeau
2008-09-14	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-13	Remove redefinition of id in Program.Basics, just add maximal implicits.	msozeau
2008-09-12	Add a type argument to letin_tac instead of using casts and recomputing	msozeau
2008-09-11	Fixes in dependent induction tactic, putting things in better order for	msozeau
2008-09-09	Fix a bug reintroduced in [setoid_reflexivity] etc...	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau