aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Int31/Int31.v
AgeCommit message (Expand)Author
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-02-04Primitive integersMaxime Dénès
2018-11-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
2018-09-22Fix typo in comment.Nick Lewycky
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-10Declaring Scope prior to loading primitive printers.Hugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-13Fix some typos.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
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-08-17Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingglondu
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-19Ring31 : a ring structure and tactic for int31letouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-02newton iteration for sqrt31thery
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-05-26Int31 : gcd31 was wrongletouzey
2008-05-23(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...letouzey
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good id...letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
2008-05-16More BigNum cleanup: letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:46:16 +0000