aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/BigNumPrelude.v
AgeCommit message (Expand)Author
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2008-06-28QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...letouzey
2008-06-25Some work on BigQ :letouzey
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey