coq - The formal proof system

Age	Commit message (Expand)	Author
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-04-21	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau
2009-04-20	Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that	msozeau
2009-04-18	Just export RelationClasses for [Equivalence] through Setoid.	msozeau
2009-04-17	Only export the notations of Morphism as well as Equivalence through	msozeau
2009-04-16	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau
2009-04-14	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau
2009-04-14	Some additions in Max and Zmax. Unifiying list of statements and names	herbelin
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-08	Experimental support for automatic destruction of recursive calls and	msozeau
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-04-03	Ocamlbuild: improvements suggested by N. Pouillard	letouzey
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-28	ZArith/Int: no need to load romega here (but rather in FullAVL)	letouzey
2009-03-27	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey
2009-03-18	fixed ring/field warning about hyp cleaning up	barras
2009-03-17	- gros commit sur ring et field: passage des arguments simplifie	barras
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-02-10	Cyclic31: proof of a forgotten admit	letouzey
2009-02-06	Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]	herbelin
2009-02-04	Fix [subrelation] clauses that privileged the weakest. Better impl args	msozeau
2009-02-04	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau
2009-01-28	FSet(Weak)List : eq_dec becomes Defined (and gets better proof)	letouzey
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2009-01-21	- Better deal with commands inside section titles in latex output using	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-18	Last changes in type class syntax:	msozeau
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-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	FMaps: various updates (mostly suggested by P. Casteran)	letouzey
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-22	FMap: fold_rec + more permissive transpose hyp + various cleanup	letouzey
2008-12-18	FSets: integration of suggestions by P. Casteran and S. Lescuyer	letouzey
2008-12-17	Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e...	letouzey
2008-12-17	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-12-16	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau
2008-12-16	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-12	Uniformity with the rest of the StdLib : _symm --> _sym	letouzey
2008-12-11	Structural definition of PositiveMap.fold	glondu
2008-12-11	Make PositiveMap.xmapi structural	glondu
2008-12-08	Fix handling of [inverse] in setoid_rewrite, with an hopefully complete	msozeau
2008-12-04	Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson	msozeau