aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith
Commit message (Expand)AuthorAge
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* 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
* Smaller proof terms for QcPower_{0,pos}Gravatar glondu2011-08-17
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* First release of Vector library.Gravatar pboutill2010-12-10
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* 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
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* changed deprecated setoid into relationGravatar amahboub2009-08-05
* (Try to) use the conversion oracle also in w_unify to choose which constant toGravatar msozeau2008-10-03
* Oups (on refait le 11268 en mieux)Gravatar herbelin2008-07-27
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Autour du parsing:Gravatar herbelin2008-07-15
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Add Morphisms for Qceiling and QfloorGravatar roconnor2008-02-05
* small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...Gravatar letouzey2007-11-24
* 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
* - renaming Qle_shift_recip_r into Qle_shift_inv_r, etcGravatar roconnor2007-09-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 22:00:57 +0000