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