aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...Gravatar aspiwack2011-08-09
* Some forgotten lemma in Arith with "O" in the name instead of "0".Gravatar herbelin2011-08-08
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
* All the parameters of Compare are implicits.Gravatar pboutill2011-07-26
* All the parameters of or can be implicits.Gravatar pboutill2011-07-26
* Same Implicit Arguments rule for sumbool and sumor.Gravatar pboutill2011-07-26
* Some facts about functional extensionality (especially alternativeGravatar herbelin2011-07-16
* More lemmas relating the different equivalent formulations of eq_dep.Gravatar herbelin2011-07-16
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
* Added a characterization of unique existence.Gravatar herbelin2011-07-16
* StrictOrder marked explicitly to be in PropGravatar letouzey2011-07-04
* Some cleanup of ZcomplementsGravatar letouzey2011-07-01
* 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
* Some cleanup of Wf_Z.vGravatar letouzey2011-06-28
* Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)Gravatar letouzey2011-06-27
* Znumtheory: a correct version of a compatibility Zdivide_introGravatar letouzey2011-06-27
* 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
* cleanup of ZsgnGravatar letouzey2011-06-23
* cleanup of Zmin and ZmaxGravatar letouzey2011-06-23
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* Some migration of results from BinInt to NumbersGravatar letouzey2011-06-20
* Zcompare.destr_zcompare subsumed by case Z.compare_specGravatar letouzey2011-06-20
* Clean-up of Zcompare and ZorderGravatar letouzey2011-06-20
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Some simplifications in NZDomainGravatar letouzey2011-06-20
* Making printing of backtick in Program reparsable (avoiding collision with "`(")Gravatar herbelin2011-06-14
* Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.Gravatar msozeau2011-06-07
* BinNat: N.binary_rect is now a definition instead of an opaque proofGravatar letouzey2011-05-05
* Peano recursion for positive: integration of Daniel Schepler's codeGravatar letouzey2011-05-05
* Minimal lemmas about Z.gt, N.gt and coGravatar letouzey2011-05-05
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of NnatGravatar letouzey2011-05-05
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* BinNatDef containing all functions of BinNat, misc adaptations in BinPosGravatar letouzey2011-05-05
* BinPosDef: a module with all code about positive, later Included in BinPosGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Modularization of PnatGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 09:45:00 +0000