| Commit message (Expand) | Author | Age |
|---|
| * | Keep the Z_scope local to this file. |  roconnor | 2008-01-24 |
| * | Changing R to a local definition so that it isn't exported. | roconnor | 2008-01-23 |
| * | Typo |  notin | 2008-01-23 |
| * | Adding Zdiv_le_compat_l |  thery | 2008-01-22 |
| * | Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ... |  msozeau | 2008-01-18 |
| * | Change notation for setoid inequality, coerce objects before comparing them. ... | msozeau | 2008-01-18 |
| * | Fix Makefile bug, using .v instead of .vo and document SetoidDec.v | msozeau | 2008-01-17 |
| * | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
| * | Bug in sqrt321 | thery | 2008-01-17 |
| * | Generalize instance declarations to any context, better name handling. Add ho... | msozeau | 2008-01-15 |
| * | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau | 2008-01-07 |
| * | Remove spurious .d, better tactics. | msozeau | 2008-01-07 |
| * | Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ... | msozeau | 2008-01-05 |
| * | more user-friendly versions of some properties lemmas in FSets/FMap |  letouzey | 2008-01-04 |
| * | Add partial setoids in theories/Classes, add SetoidDec class for setoids with... | msozeau | 2008-01-04 |
| * | Implicit arguments in class field declarations | msozeau | 2008-01-02 |
| * | Better resolution of implicit parameters in typeclass binders, add extensiona... | msozeau | 2008-01-02 |
| * | 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-31 |
| * | 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-21 |
| * | Quelques arguments en plus... |  glondu | 2007-12-17 |
| * | migration of ide/utf8.v to theories/Unicode/Utf8.v | letouzey | 2007-12-13 |
| * | 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 |
roconnor
notin
thery
msozeau
letouzey
glondu
emakarov
jforest