diff options
Diffstat (limited to 'parsing/esyntax.mli')
| -rw-r--r-- | parsing/esyntax.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index 5ddadb5bc..8e3445ed7 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -42,7 +42,7 @@ module Ppprim : val add : string * t -> unit end -val declare_infix_symbol : Names.section_path -> string -> unit +val declare_infix_symbol : Libnames.section_path -> string -> unit (* Generic printing functions *) val token_printer: std_printer -> std_printer |