diff options
| -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) = |