aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Ints/Z
Commit message (Expand)AuthorAge
* Report des quelques modifs faites avec Pierre Letouzey sur lesGravatar herbelin2008-04-27
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* Adding BigQ and proofsGravatar thery2007-10-25
* Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...Gravatar emakarov2007-10-04
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* add_mul_pos uses int31 onlyGravatar thery2007-05-21
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11