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_zsyntax.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_zsyntax.ml')
| -rw-r--r-- | parsing/g_zsyntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index e6cbda712..cae9c76f2 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -223,7 +223,7 @@ let uninterp_positive p = (* Declaring interpreters and uninterpreters for positive *) (************************************************************************) -let _ = Symbols.declare_numeral_interpreter "positive_scope" +let _ = Notation.declare_numeral_interpreter "positive_scope" (glob_positive,positive_module) (interp_positive,Some pat_interp_positive) ([RRef (dummy_loc, glob_xI); @@ -284,7 +284,7 @@ let uninterp_n p = (************************************************************************) (* Declaring interpreters and uninterpreters for N *) -let _ = Symbols.declare_numeral_interpreter "N_scope" +let _ = Notation.declare_numeral_interpreter "N_scope" (glob_n,binnat_module) (n_of_int,Some pat_n_of_int) ([RRef (dummy_loc, glob_N0); @@ -340,7 +340,7 @@ let uninterp_z p = (************************************************************************) (* Declaring interpreters and uninterpreters for Z *) -let _ = Symbols.declare_numeral_interpreter "Z_scope" +let _ = Notation.declare_numeral_interpreter "Z_scope" (glob_z,fast_integer_module) (z_of_int,Some pat_z_of_int) ([RRef (dummy_loc, glob_ZERO); |