aboutsummaryrefslogtreecommitdiff
path: root/interp/syntax_def.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/syntax_def.ml')
-rw-r--r--interp/syntax_def.ml2
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