coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	A result about Zsgn(a/b), both for Zdiv and ZOdiv	letouzey	2007-11-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10313 85f007b7-540e-0410-9357-904b9bb8a0f7
*	First reasonably complete version of ZOdiv, including some properties	letouzey	2007-11-10
\| \| \| \| \| \| \| \| \| \| \|	that aren't so nice after all. For instance, ((a+b*c) mod c) might differ from (a mod c), due to sign issues. Minor improvements to Zdiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 ↵	jforest	2007-11-09
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	more about ZOdiv and ZOmod (still not finished)	letouzey	2007-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10307 85f007b7-540e-0410-9357-904b9bb8a0f7
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
	A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7