| Commit message (Expand) | Author | Age |
|---|
| * | Modularization of BinPos + fixes in Stdlib |  letouzey | 2011-05-05 |
| * | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
| * | First release of Vector library. |  pboutill | 2010-12-10 |
| * | Updated all headers for 8.3 and trunk |  herbelin | 2010-07-24 |
| * | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Min, Max: for avoiding inelegant NPeano.max printing, we Export this lib | letouzey | 2010-02-10 |
| * | DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation | letouzey | 2010-02-08 |
| * | Ring31 : a ring structure and tactic for int31 | letouzey | 2010-01-19 |
| * | Forgot a file in last commit. |  msozeau | 2009-12-06 |
| * | Fix anomaly when using typeclass resolution with filtered hyps in evars. | msozeau | 2009-12-06 |
| * | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey | 2009-11-12 |
| * | Simplification of Numbers, mainly thanks to Include | letouzey | 2009-11-10 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Cyclic31: proof of a forgotten admit | letouzey | 2009-02-10 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | newton iteration for sqrt31 |  thery | 2008-06-02 |
| * | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey | 2008-06-01 |
| * | Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are | letouzey | 2008-05-28 |
| * | CyclicAxioms: after discussion with Laurent, znz_WW and variants are | letouzey | 2008-05-28 |
| * | Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left ! | letouzey | 2008-05-28 |
| * | Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin... | letouzey | 2008-05-27 |
| * | Correction du problème de complexité de Print Assumptions : | aspiwack | 2008-05-27 |
| * | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey | 2008-05-27 |
| * | Cyclic31 : proof of the spec of gcd31 | letouzey | 2008-05-27 |
| * | Int31 : gcd31 was wrong | letouzey | 2008-05-26 |
| * | Cyclic31: cleanup, 2 Admitted killed (6 remaining) | letouzey | 2008-05-26 |
| * | Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ... | letouzey | 2008-05-23 |
| * | (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms... | letouzey | 2008-05-23 |
| * | writing a match on a digit via syntax "if ... then ... else" is not a good id... | letouzey | 2008-05-22 |
| * | Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui... | letouzey | 2008-05-22 |
| * | ZModulo: Z viewed modulo 2^digits implements CyclicAxioms | letouzey | 2008-05-17 |
| * | Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate | letouzey | 2008-05-16 |
| * | BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZ | letouzey | 2008-05-16 |
| * | More BigNum cleanup: | letouzey | 2008-05-16 |
| * | Coq headers + $ in theories/Numbers files | letouzey | 2008-05-15 |
| * | Integration of theories/Ints into theories/Numbers, part 1: moving files | letouzey | 2008-05-07 |
letouzey
pboutill
herbelin
aspiwack
msozeau
glondu
thery