aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/Int31/Cyclic31.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
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* 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
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* First release of Vector library.Gravatar pboutill2010-12-10
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Min, Max: for avoiding inelegant NPeano.max printing, we Export this libGravatar letouzey2010-02-10
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* Forgot a file in last commit.Gravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Cyclic31: proof of a forgotten admitGravatar letouzey2009-02-10
* newton iteration for sqrt31Gravatar thery2008-06-02
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are Gravatar letouzey2008-05-28
* CyclicAxioms: after discussion with Laurent, znz_WW and variants areGravatar letouzey2008-05-28
* Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !Gravatar letouzey2008-05-28
* Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...Gravatar letouzey2008-05-27
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
* Cyclic31: cleanup, 2 Admitted killed (6 remaining)Gravatar letouzey2008-05-26
* Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...Gravatar letouzey2008-05-23
* (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...Gravatar letouzey2008-05-23
* Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateGravatar letouzey2008-05-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 18:27:26 +0000