| Age | Commit message (Expand) | Author |
|---|
| 2008-01-04 | Add partial setoids in theories/Classes, add SetoidDec class for setoids with... | msozeau |
| 2008-01-02 | Implicit arguments in class field declarations | msozeau |
| 2008-01-02 | Better resolution of implicit parameters in typeclass binders, add extensiona... | msozeau |
| 2007-12-31 | Move Classes.Setoid to Classes.SetoidClass to avoid name clash. | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-21 | Pour éviter des erreus lors de make doc dues à du code source non taggé en... | notin |
| 2007-12-21 | Deux petits théorèmes utiles dans Minus.v | notin |
| 2007-12-17 | Quelques arguments en plus... | glondu |
| 2007-12-13 | migration of ide/utf8.v to theories/Unicode/Utf8.v | letouzey |
| 2007-12-07 | Petit oubli de thery. | glondu |
| 2007-12-06 | Adding MemoFunction + Lowering Height | thery |
| 2007-11-24 | * A few Parameter Inline, but they dont seem to help much concerning | letouzey |
| 2007-11-24 | small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough... | letouzey |
| 2007-11-22 | An update on Numbers. Added two files dealing with recursion, for information... | emakarov |
| 2007-11-21 | extensible version | thery |
| 2007-11-16 | Added theorems; created NZPlusOrder from NTimesOrder. | emakarov |
| 2007-11-15 | Split NTimesOrder into properly NTimesOrder and NPlusOrder. | emakarov |
| 2007-11-14 | Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder... | emakarov |
| 2007-11-10 | A result about Zsgn(a/b), both for Zdiv and ZOdiv | letouzey |
| 2007-11-10 | First reasonably complete version of ZOdiv, including some properties | letouzey |
| 2007-11-09 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0... | jforest |
| 2007-11-09 | more about ZOdiv and ZOmod (still not finished) | letouzey |
| 2007-11-08 | Corrected the ML code for well-founded recursion in the comment. | emakarov |
| 2007-11-08 | Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic. | emakarov |
| 2007-11-08 | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey |
| 2007-11-07 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0... | emakarov |
| 2007-11-07 | Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v. | emakarov |
| 2007-11-07 | Replaced BinNat with a new version that is based on theories/Numbers/Natural/... | emakarov |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
| 2007-11-06 | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey |
| 2007-11-03 | An update of theories/Numbers | emakarov |
| 2007-11-01 | two additionnal results on list append (coming from theories/ints/List/ListAu... | letouzey |
| 2007-11-01 | A way to specialize universally quantified hypothesis: if H is | letouzey |
| 2007-11-01 | Adding Qround.v (and helper lemmas and hints) | roconnor |
| 2007-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 2007-10-30 | temporary workaround for bug #1738 | letouzey |
| 2007-10-30 | A useless Add Morphism: since Subset is a Setoid Relation, it is also | letouzey |
| 2007-10-30 | Changement esthétique de la preuve de mult_is_one | notin |
| 2007-10-30 | Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et plus_is... | notin |
| 2007-10-29 | Revision of the FSetWeak Interface, so that it becomes a precise | letouzey |
| 2007-10-25 | Adding BigQ and proofs | thery |
| 2007-10-24 | Addition of more general tactics for equality. Functional extensionality and ... | msozeau |
| 2007-10-23 | Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu... | emakarov |
| 2007-10-21 | Cleanup attempt of Hints in *Interface.v files. | letouzey |
| 2007-10-19 | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor |
| 2007-10-16 | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov |
| 2007-10-05 | Added the automatic generation of the boolean equality if possible and the | vsiles |
| 2007-10-04 | Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o... | emakarov |
| 2007-10-03 | Révision de theories/Logic concernant les axiomes de descriptions. | herbelin |
| 2007-10-03 | BigZ now are proved | thery |
