aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic
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
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* 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
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* 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
* 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
* 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
* Cleanup of NdigitsGravatar letouzey2011-06-30
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)Gravatar letouzey2011-03-30
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* First release of Vector library.Gravatar pboutill2010-12-10
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fix compilation by replacing some "auto with zarith" with "ring"Gravatar glondu2010-06-28
* 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
* Numbers: separation of funs, notations, axioms. Notations via module, without...Gravatar letouzey2010-01-07
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* 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
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* 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
* Numbers: more (syntactic) changes toward new style of type classesGravatar letouzey2009-11-06
* Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcGravatar letouzey2009-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 00:03:51 +0000