| Age | Commit message (Expand) | Author |
|---|
| 2008-02-08 | better comments in FMapInterface | letouzey |
| 2008-02-08 | better comments in FSetInterface | letouzey |
| 2008-02-08 | Change implementation of resolution for typeclasses to use a customized | msozeau |
| 2008-02-08 | more complete FSets.v | letouzey |
| 2008-02-08 | one forgotten compatibility lemma | letouzey |
| 2008-02-06 | Fix obligations not being discharged due to new definition of complement. | msozeau |
| 2008-02-06 | New algorithm to resolve morphisms, after discussion with Nicolas | msozeau |
| 2008-02-05 | kill some useless module aliases E:=X (for better name printing, see Elie's 1... | letouzey |
| 2008-02-05 | Add Morphisms for Qceiling and Qfloor | roconnor |
| 2008-02-04 | Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps | letouzey |
| 2008-02-03 | Add new files theories/Program/Basics.v and theories/Classes/Relations.v | msozeau |
| 2008-02-02 | factorization part II (Properties + EqProperties), inclusion of FSetDecide (f... | letouzey |
| 2008-02-01 | Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak... | letouzey |
| 2008-01-31 | Debug implementation of dependent induction/dependent destruction and documen... | msozeau |
| 2008-01-30 | Work on dependent induction tactic and friends, finish the test-suite example | msozeau |
| 2008-01-30 | Support for occurences and 'in' in class_setoid, work on corresponding tactic... | msozeau |
| 2008-01-24 | Nicer proofs. | roconnor |
| 2008-01-24 | remove Fourier Failure warnings. | roconnor |
| 2008-01-24 | Prove the decidability of arithmetical statements using the real numbers. | roconnor |
| 2008-01-24 | Keep the Z_scope local to this file. | roconnor |
| 2008-01-23 | Changing R to a local definition so that it isn't exported. | roconnor |
| 2008-01-23 | Typo | notin |
| 2008-01-22 | Adding Zdiv_le_compat_l | thery |
| 2008-01-18 | 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-17 | 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-15 | Generalize instance declarations to any context, better name handling. Add ho... | msozeau |
| 2008-01-07 | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau |
| 2008-01-07 | Remove spurious .d, better tactics. | msozeau |
| 2008-01-05 | Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ... | msozeau |
| 2008-01-04 | 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-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 |
