From 286d7e8201de98dc5cc36b6fbda8f9c1126f37ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Apr 2008 23:51:06 +0000
Subject: Definition of N moves back to BinNat (partial backtrack of commits
 10298-10300)

This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_zsyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 6c20107f3a..5d57c49dbb 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -96,7 +96,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let binnat_module = ["Coq";"Numbers";"Natural";"Binary";"NBinDefs"]
+let binnat_module = ["Coq";"NArith";"BinNat"]
 let n_kn = make_kn (make_dir binnat_module) (id_of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
-- 
cgit v1.2.3