aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/Int31/Int31.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingGravatar glondu2011-08-17
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* newton iteration for sqrt31Gravatar thery2008-06-02
* Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are Gravatar letouzey2008-05-28
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* Int31 : gcd31 was wrongGravatar letouzey2008-05-26
* (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...Gravatar letouzey2008-05-23
* writing a match on a digit via syntax "if ... then ... else" is not a good id...Gravatar letouzey2008-05-22
* Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...Gravatar letouzey2008-05-22
* ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsGravatar letouzey2008-05-17
* BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZGravatar letouzey2008-05-16
* More BigNum cleanup: Gravatar letouzey2008-05-16
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 02:51:22 +0000