From 929f9de11b22612ee3809a37222e417250ccda4f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Dec 2013 19:19:24 +0100
Subject: Disable GlobRef feedback (CoqIDE does nothing with them)

The original idea was to send not the kernel name, but the file/line
to that CoqIDE could make the text an hyperlink to the file, exactly
as coqdoc generated HTML.
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 259690aa97..5731d7d044 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -725,7 +725,7 @@ let feedback_global loc ref =
     Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty))
 
 let dump_extended_global loc = function
-  | TrueGlobal ref -> feedback_global loc ref; Dumpglob.add_glob loc ref
+  | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref
   | SynDef sp -> Dumpglob.add_glob_kn loc sp
 
 let intern_extended_global_of_qualid (loc,qid) =
-- 
cgit v1.2.3