diff options
| author | herbelin | 2005-01-02 08:47:14 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-02 08:47:14 +0000 |
| commit | 2dee039338e6f130447741b67f36eba666131b8a (patch) | |
| tree | b7ac63eb7f7cc87edfa0056e7c69653fd6c802a1 /interp/syntax_def.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 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 52fcb53914..f2a31f9de5 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -39,7 +39,7 @@ let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) = add_syntax_constant kn c; Nametab.push_syntactic_definition (Nametab.Until i) sp kn; if not onlyparse then - Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c) + Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c) let open_syntax_constant i ((sp,kn),c) = Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn |