| Commit message (Expand) | Author | Age |
|---|
| * | Petit oubli de thery. |  glondu | 2007-12-07 |
| * | Adding MemoFunction + Lowering Height |  thery | 2007-12-06 |
| * | * 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-24 |
| * | An update on Numbers. Added two files dealing with recursion, for information... |  emakarov | 2007-11-22 |
| * | extensible version | thery | 2007-11-21 |
| * | Added theorems; created NZPlusOrder from NTimesOrder. | emakarov | 2007-11-16 |
| * | Split NTimesOrder into properly NTimesOrder and NPlusOrder. | emakarov | 2007-11-15 |
| * | Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder... | emakarov | 2007-11-14 |
| * | 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-10 |
| * | 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-09 |
| * | 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-08 |
| * | 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-07 |
| * | 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-06 |
| * | An update of theories/Numbers | emakarov | 2007-11-03 |
| * | 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-11-01 |
| * | 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-30 |
| * | Revision of the FSetWeak Interface, so that it becomes a precise | letouzey | 2007-10-29 |
| * | Adding BigQ and proofs | thery | 2007-10-25 |
| * | Addition of more general tactics for equality. Functional extensionality and ... |  msozeau | 2007-10-24 |
| * | Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu... | emakarov | 2007-10-23 |
| * | Cleanup attempt of Hints in *Interface.v files. | letouzey | 2007-10-21 |
| * | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor | 2007-10-19 |
| * | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov | 2007-10-16 |
| * | Added the automatic generation of the boolean equality if possible and the |  vsiles | 2007-10-05 |
| * | Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o... | emakarov | 2007-10-04 |
| * | Révision de theories/Logic concernant les axiomes de descriptions. |  herbelin | 2007-10-03 |
| * | BigZ now are proved | thery | 2007-10-03 |
| * | The following now compiles: abstract integers with plus, minus and times, bin... | emakarov | 2007-10-02 |
| * | Now NMake is proved | thery | 2007-10-02 |
| * | Added the compilation of theories/Numbers to Makefile.common. The following t... | emakarov | 2007-10-01 |
| * | Nouvelle mise à jour | herbelin | 2007-10-01 |
| * | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin | 2007-09-30 |
| * | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu | 2007-09-28 |
| * | Oubli dans Setoid.v | notin | 2007-09-28 |
| * | Découpage de Setoid.v | notin | 2007-09-27 |
| * | Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0 | herbelin | 2007-09-27 |
glondu
thery
letouzey
emakarov
jforest
roconnor
notin
msozeau
vsiles
herbelin