diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
| commit | 42ea537affb88f8e63499d909eb526e024fc0aec (patch) | |
| tree | 15d95ea521cd5b5ee592cee7c818cf45b413debf /tools | |
| parent | fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa (diff) | |
Fix "Existing Instance" to handle globality information and "Existing
Class" too to handle references instead of just idents. Minor fix in
coqdoc. zeta-normalize setoid_rewrite proofs, removing useless
let-bindings generated by the tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
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 90d0d0e00..515d9519f 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 "}{" *) |