diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-27 19:19:24 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-05 16:55:58 +0100 |
| commit | 929f9de11b22612ee3809a37222e417250ccda4f (patch) | |
| tree | fde8fde029d7fc4c2d776ecf81941ac7ebc11405 | |
| parent | d5e353ded3282b2cb2314e8ee59315e3d14c4ce1 (diff) | |
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.
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 259690aa9..5731d7d04 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) = |