diff options
Diffstat (limited to 'toplevel/himsg.mli')
| -rw-r--r-- | toplevel/himsg.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 5c5548c2a..ff3eac8ee 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -21,7 +21,7 @@ end (*s The result is a module which provides a function [explain_type_error] to explain a type error for a given kind in a given context, which are usually the three arguments carried by the exception [TypeError] - (see \citesec{typeerrors}). *) + (see \refsec{typeerrors}). *) module Make (P : Printer) : sig |