aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-26 14:02:04 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-26 14:02:04 +0000
commitafc087182a5b44f08de1c90d84293648c35ecc5c (patch)
tree3a9db1080c19db0df102ca2680f43cd69d1bf353 /tools/coqdoc/output.ml
parent8ebcb152ca0cf260fe1980758e4434c74926d78e (diff)
Oubli lors de la révision #11177
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index a75b7196d..a5378e9df 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -443,7 +443,6 @@ module Html = struct
printf "</span>"
end else
begin
- Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc;
try
(match Index.find !current_module loc with
| Def (fullid,_) ->