diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 90d0d0e007..515d9519f8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -262,7 +262,7 @@ module Latex = struct (printf "\\coqref{"; label_ident id; printf "}{\\coqdoc%s{" (type_name typ); raw_ident s; printf "}}") | External m when !externals -> - printf "\\coqexternalref{"; label_ident m; printf "}{"; + printf "\\coqexternalref{"; raw_ident m; printf "}{"; label_ident fid; printf "}{\\coqdoc%s{" (type_name typ); raw_ident s; printf "}}" | External _ | Unknown -> (* printf "\\coqref{"; label_ident id; printf "}{" *) |