coq - The formal proof system

Age	Commit message (Expand)	Author
2009-04-27	Cleanup old eauto code.	msozeau
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
2009-04-27	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-04-24	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin
2009-04-21	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau
2009-04-17	- Fix handling of clauses in setoid_rewrite to rewrite under binders	msozeau
2009-04-16	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau
2009-04-16	nouvelle version de la tactique groebner proposee par Loic:	barras
2009-04-14	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau
2009-04-14	Add a combinator for rewriting given a list of terms and fix the	msozeau
2009-04-13	Rewrite of setoid_rewrite to modularize it based on proof-producing	msozeau
2009-04-10	Fix premature optimisation in dependent induction: even variable args need	msozeau
2009-04-10	Fix tauto no longer failing after commit 12077; appropriate error	herbelin
2009-04-09	Turning tauto into a classical tautology prover as soon as classical	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey
2009-04-08	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-04-05	Display the content of the list instead of "<list>" when an idtac	herbelin
2009-03-31	Fix auto so that Extern tactics associated to no patterns can apply to	msozeau
2009-03-28	Fix useless redeclaration of a tactic name when UpdateTac is replayed.	msozeau
2009-03-22	Backport from v8.2 branch of 11986 (interpretation of quantified	herbelin
2009-03-22	Compromise wrt introduction-names compatibility issue after addition	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-03-19	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
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