diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-02 08:47:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-02 08:47:14 +0000 |
| commit | 2dee039338e6f130447741b67f36eba666131b8a (patch) | |
| tree | b7ac63eb7f7cc87edfa0056e7c69653fd6c802a1 /parsing/g_natsyntax.ml | |
| parent | da705691fc9cf7724f78f4ed0cc8b93c4d7bc08e (diff) | |
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de printers dans ocamldebug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_natsyntax.ml')
| -rw-r--r-- | parsing/g_natsyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index 8fe0536eb..85b79d8bf 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -111,7 +111,7 @@ open Rawterm open Libnames open Bigint open Coqlib -open Symbols +open Notation open Pp open Util open Names @@ -187,7 +187,7 @@ let uninterp_nat_pattern p = (* Declare the primitive parsers and printers *) let _ = - Symbols.declare_numeral_interpreter "nat_scope" + Notation.declare_numeral_interpreter "nat_scope" (glob_nat,["Coq";"Init";"Datatypes"]) (nat_of_int,Some pat_nat_of_int) ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None) |