aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/vo.itarget
AgeCommit message (Collapse)Author
2010-02-09Numbers: properties of min/max with respect to 0,S,P,add,sub,mulletouzey
With these properties, we can kill Arith/MinMax, NArith/Nminmax, and leave ZArith/Zminmax as a compatibility file only. Now the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN contains all theses facts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake: several things need not be macro-generatedletouzey
The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-19Ring31 : a ring structure and tactic for int31letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Numbers: axiomatization + generic properties of abs and sgn.letouzey
This allow to really finish files about division. An abs and sgn is added to BigZ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. ↵letouzey
Boute Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"): - ZDivFloor.v for Coq historical division (former ZDivCoq.v) - ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v) - ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v) These property functors are more or less finished (except that sign and abs stuff should be migrated to a separate file). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
- For Z, we propose 3 conventions for the sign of the remainder... - Instanciation for nat in NPeano. - Beginning of instanciation in ZOdiv. Still many proofs to finish, etc, etc, but soon we will have a decent properties database for all divisions of all instances of Numbers (e.g. BigZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-10NZDomain: investigation of the shape of NZ domain, more results about ↵letouzey
ofnat:nat->NZ.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12575 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵letouzey
in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 12:21:21 +0000