coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-17	- gros commit sur ring et field: passage des arguments simplifie	barras
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-23	Add support for dependent "destruct" over terms in dependent types.	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-16	Fix [apply_in] which short-circuited resolution of evars in a custom	msozeau
2009-02-06	pushed evar reduction in kernel	barras
2009-02-04	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau
2009-01-29	Solves some warning and hides some not-bad ones in doc. It remains a	herbelin
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
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-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau
2009-01-11	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin
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