diff options
Diffstat (limited to 'doc/refman/RefMan-tus.tex')
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 3e2988676..797b0aded 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -1012,7 +1012,7 @@ the different kinds of errors used in \Coq{} : \fun{val Std.error : string -> 'a} {For simple error messages} -\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a} +\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a} {See Section~\ref{PrettyPrinter} : this can be used if the user want to display a term or build a complex error message} |