aboutsummaryrefslogtreecommitdiff
path: root/theories/Ints/num/NMake.v
AgeCommit message (Expand)Author
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-27Report des quelques modifs faites avec Pierre Letouzey sur lesherbelin
2008-04-27- Fix bug in unification not taking into account the right metamsozeau
2007-12-06Adding MemoFunction + Lowering Heightthery
2007-10-03BigZ now are provedthery
2007-10-02Now NMake is provedthery
2007-07-30mul and sqrtthery
2007-07-24proof of compare addedthery
2007-07-12Proof for subthery
2007-07-12Proof for succ, add, predthery
2007-06-19safe_shift correct recursionthery
2007-06-19safe_shift recursionthery
2007-06-19Adding function is_even, safe_shiftl, safe_shiftrthery
2007-06-18Correct height computationthery
2007-05-21add_mul_pos uses int31 onlythery
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack