aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* 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
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Fixing bug #3270. Patch by Robbert Krebbers.Gravatar Pierre-Marie Pédrot2014-07-08
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - 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
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Give inner fixpoint of gcd31 a name, to avoid excessive unfoldingGravatar glondu2011-08-17
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Cleanup in SpecViaZGravatar letouzey2011-06-30
* Cleanup of NdigitsGravatar letouzey2011-06-30
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* Deletion of useless Zlog_defGravatar letouzey2011-06-28
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defGravatar letouzey2011-06-28
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* Numbers: a particular case of div_uniqueGravatar letouzey2011-06-24
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* Some migration of results from BinInt to NumbersGravatar letouzey2011-06-20
* Zcompare.destr_zcompare subsumed by case Z.compare_specGravatar letouzey2011-06-20
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20