aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Expand)AuthorAge
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.Gravatar herbelin2009-10-04
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.Gravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* adds a theorem to reason at the level of ZGravatar bertot2009-05-07
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
* ZArith/Int: no need to load romega here (but rather in FullAVL)Gravatar letouzey2009-03-28
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Zdiv: eqm (equality modulo some N) can now be declared as Parametric RelationGravatar letouzey2008-10-20
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* Oops... forgot some debug code.Gravatar msozeau2008-07-23
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* Zpow_facts.Zmult_power: kills a useless hypothesisGravatar letouzey2008-06-11
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* one forgotten compatibility lemmaGravatar letouzey2008-02-08
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* A result about Zsgn(a/b), both for Zdiv and ZOdivGravatar letouzey2007-11-10
* First reasonably complete version of ZOdiv, including some propertiesGravatar letouzey2007-11-10
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...Gravatar jforest2007-11-09
* more about ZOdiv and ZOmod (still not finished)Gravatar letouzey2007-11-09
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:54:13 +0000