coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-10	Misc fixes:	msozeau
2009-09-09	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-09-03	Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as	msozeau
2009-08-31	Fix notation for ~x in theories/Unicode/Utf8.v	glondu
2009-08-24	New tactic to rewrite decidability lemmas when one knows which side	herbelin
2009-08-19	adds a property on map	bertot
2009-08-19	adds lemmas on interactions between existsb, forallb, and app	bertot
2009-08-11	Fixed extra space in printing notation { x & P } + minor other things	herbelin
2009-08-05	changed deprecated setoid into relation	amahboub
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-07-24	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey
2009-07-24	List: add a iff-based lemma about In and ++	letouzey
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-07-22	Better comparison functions in OrderedTypeEx	letouzey
2009-07-20	Use unfold directly in unfold_equations. Fixes test-suite.	msozeau
2009-07-20	Typo in a comment	letouzey
2009-07-14	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau
2009-06-29	Miscellaneous practical commits:	herbelin
2009-06-22	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras
2009-06-08	Do a fixpoint on the result of typeclass search to force the	msozeau
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-06-06	Very-small-step policy changes to the library.	herbelin
2009-06-02	Use Type instead of Set.	msozeau
2009-05-27	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau
2009-05-20	Many fixes in unification:	msozeau
2009-05-16	Minor fixes in typeclasses:	msozeau
2009-05-07	adds a theorem to reason at the level of Z	bertot
2009-05-05	Improvements in typeclasses eauto and generalized rewriting:	msozeau
2009-04-28	Fixes for bugs in r12110:	msozeau
2009-04-28	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin
2009-04-27	- Implementation of a new typeclasses eauto procedure based on success	msozeau
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