aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/Abstract/NMinus.v
AgeCommit message (Collapse)Author
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
for increased consistency with bignums parts (commit part II: names of files + additional translation minus --> sub) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
for increased consistency with bignums parts (commit part I: content of files) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
of the fix I added an optional "by" annotation for rewrite to solve said conditions in the same tactic call. Most of the theories have been updated, only FSets is missing, Pierre will take care of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-22An update on Numbers. Added two files dealing with recursion, for ↵emakarov
information only. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-14Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ↵emakarov
ZArith/Zorder on MacOS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10304 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-07Replaced BinNat with a new version that is based on ↵emakarov
theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-03An update of theories/Numbersemakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10285 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Added Numbers/Natural/Abstract/NIso.v that proves that any two models of ↵emakarov
natural numbers are isomorphic. Added NatScope and IntScope for abstract developments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Added the compilation of theories/Numbers to Makefile.common. The following ↵emakarov
things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25An update on theories/Numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10142 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Update on theories/Numbers. Natural numbers are mostly complete,emakarov
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 21:25:10 +0000