| Commit message (Expand) | Author | Age |
* | Integration of theories/Ints into theories/Numbers, part 1: moving files | letouzey | 2008-05-07 |
* | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau | 2008-04-28 |
* | Report des quelques modifs faites avec Pierre Letouzey sur les | herbelin | 2008-04-27 |
* | - Fix bug in unification not taking into account the right meta | msozeau | 2008-04-27 |
* | - Add pretty-printers for Idpred, Cpred and transparent_state, used for | msozeau | 2008-04-24 |
* | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
* | Adding Zdiv_le_compat_l | thery | 2008-01-22 |
* | Bug in sqrt321 | thery | 2008-01-17 |
* | Pour éviter des erreus lors de make doc dues à du code source non taggé en... | notin | 2007-12-21 |
* | Petit oubli de thery. | glondu | 2007-12-07 |
* | Adding MemoFunction + Lowering Height | thery | 2007-12-06 |
* | extensible version | thery | 2007-11-21 |
* | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey | 2007-11-06 |
* | In agreement with Laurent Thery, start migration of auxiliary results | letouzey | 2007-11-01 |
* | Adding BigQ and proofs | thery | 2007-10-25 |
* | Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o... | emakarov | 2007-10-04 |
* | BigZ now are proved | thery | 2007-10-03 |
* | Now NMake is proved | thery | 2007-10-02 |
* | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu | 2007-09-28 |
* | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin | 2007-09-21 |
* | mul and sqrt | thery | 2007-07-30 |
* | Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n et | notin | 2007-07-25 |
* | proof of compare added | thery | 2007-07-24 |
* | 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-18 |
* | Proof for sub | thery | 2007-07-12 |
* | normalisation (by closure) was not performed under fixpoints | barras | 2007-07-12 |
* | Proof for succ, add, pred | thery | 2007-07-12 |
* | ajout de head0 et tail0 en natif | bgregoir | 2007-06-20 |
* | safe_shift correct recursion | thery | 2007-06-19 |
* | safe_shift recursion | thery | 2007-06-19 |
* | safe_shift recursion | thery | 2007-06-19 |
* | Adding function is_even, safe_shiftl, safe_shiftr | thery | 2007-06-19 |
* | genN.ml sync | thery | 2007-06-19 |
* | Correct height computation | thery | 2007-06-18 |
* | tail0 | thery | 2007-06-06 |
* | mul_norm for Q fixed | thery | 2007-05-30 |
* | Added Z and Q implementations with int31. | aspiwack | 2007-05-21 |
* | add_mul_pos uses int31 only | thery | 2007-05-21 |
* | pos_mod fixed | thery | 2007-05-15 |
* | Correction de sqrt312 (racine carree d'un nombre represente comme un | aspiwack | 2007-05-15 |
* | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack | 2007-05-11 |