| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2007-10-02 | The following now compiles: abstract integers with plus, minus and times, bin... | emakarov |
| 2007-10-02 | Now NMake is proved | thery |
| 2007-10-01 | Added the compilation of theories/Numbers to Makefile.common. The following t... | emakarov |
| 2007-10-01 | Nouvelle mise à jour | herbelin |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2007-09-28 | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu |
| 2007-09-28 | Oubli dans Setoid.v | notin |
| 2007-09-27 | 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-26 | added a lemma to prove inj_pair2 when eq_dec is available. | vsiles |
| 2007-09-25 | An update on theories/Numbers. | emakarov |
| 2007-09-21 | Update on theories/Numbers | emakarov |
| 2007-09-21 | Update on theories/Numbers. Natural numbers are mostly complete, | emakarov |
| 2007-09-21 | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin |
| 2007-09-20 | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov |
| 2007-09-13 | Update before joining all signatures into one. | emakarov |
| 2007-09-07 | - renaming Qle_shift_recip_r into Qle_shift_inv_r, etc | roconnor |
| 2007-08-28 | Adding a few lemmas for reasoning about inequalities over the | roconnor |
| 2007-08-26 | Add more equality tactics. Upgrade program_simpl for discrimination of conjun... | msozeau |
| 2007-08-13 | An update on axiomatic number classes. | emakarov |
| 2007-08-08 | Fix dependency bugs due to Program modules renamings. | msozeau |
| 2007-08-08 | Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v | emakarov |
| 2007-08-08 | A better Program documentation. Include it in the generated stdlib doc. | msozeau |
| 2007-08-07 | Move Program tactics into a proper theories/ directory as they are general pu... | msozeau |
| 2007-07-30 | mul and sqrt | thery |
| 2007-07-25 | Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n et | notin |
| 2007-07-24 | proof of compare added | thery |
| 2007-07-24 | An update on axiomatization of numbers. | emakarov |
| 2007-07-18 | A generic preprocessing tactic zify for (r)omega | letouzey |
| 2007-07-18 | J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir | aspiwack |
| 2007-07-13 | An update on axiomatization of number classes. | emakarov |
| 2007-07-13 | Added Qpower_plus' and Zpower_Qpower | roconnor |
| 2007-07-13 | Small cleanup | letouzey |
| 2007-07-13 | Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans le | herbelin |
