diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 23:51:06 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 23:51:06 +0000 |
| commit | 286d7e8201de98dc5cc36b6fbda8f9c1126f37ea (patch) | |
| tree | 1ec5317554f488d8abd722e66a7d341d6cf521f1 /parsing/g_zsyntax.ml | |
| parent | 99ad573113f5afc8bb5409649843567dee40ba40 (diff) | |
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
Diffstat (limited to 'parsing/g_zsyntax.ml')
| -rw-r--r-- | parsing/g_zsyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 6c20107f3..5d57c49db 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) |