From f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:09 +0000 Subject: Definitions of positive, N, Z moved in Numbers/BinNums.v In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/vo.itarget | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/Numbers/vo.itarget') diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index baefbd252..c69af03fc 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -1,3 +1,4 @@ +BinNums.vo BigNumPrelude.vo Cyclic/Abstract/CyclicAxioms.vo Cyclic/Abstract/NZCyclic.vo -- cgit v1.2.3