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
---
 interp/coqlib.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ac1aa1879c..0f3d1bab2a 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -91,12 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
 let arith_dir = ["Coq";"Arith"]
 let arith_modules = [arith_dir]
 
+let numbers_dir = [ "Coq";"Numbers"]
 let parith_dir = ["Coq";"PArith"]
-
 let narith_dir = ["Coq";"NArith"]
-
 let zarith_dir = ["Coq";"ZArith"]
-let zarith_base_modules = [parith_dir;narith_dir;zarith_dir]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
 
 let init_dir = ["Coq";"Init"]
 let init_modules = [
-- 
cgit v1.2.3