coq/theories/Numbers/Integer/BigInts, branch master

Added the proof (in Numbers/Integers/TreeMod) that tree-like representation of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ.

2007-10-04T17:24:56+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10178 85f007b7-540e-0410-9357-904b9bb8a0f7

Added the compilation of theories/Numbers to Makefile.common. The following things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers.

2007-10-01T20:21:28+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7

Update on theories/Numbers. Natural numbers are mostly complete,

2007-09-21T13:22:41+00:00

need to make NZOrdAxiomsSig a subtype of NAxiomsSig.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10132 85f007b7-540e-0410-9357-904b9bb8a0f7