aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/ZModulo/ZModulo.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-15Failing on unbound notation variable in notation level modifiersHugo Herbelin
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-06-28Deletion of useless Zsqrt_defletouzey
2011-06-24Clean-up of Znumtheory, deletion of Zgcd_defletouzey
2010-10-19Add sqrt in Numbersletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-08DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationletouzey
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
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
2008-05-28CyclicAxioms: after discussion with Laurent, znz_WW and variants areletouzey
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey