diff options
| author | Pierre-Marie Pédrot | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /doc/refman | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'doc/refman')
| -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 3e29886762..797b0adedd 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} |