From 42ea537affb88f8e63499d909eb526e024fc0aec Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 27 Dec 2009 22:08:57 +0000
Subject: 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
---
 tools/coqdoc/output.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

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 "}{" *)
-- 
cgit v1.2.3