diff --git a/Makefile.config b/Makefile.config
index f1d0de558..eb571774d 100644
--- a/Makefile.config
+++ b/Makefile.config
@@ -54,6 +54,7 @@ INFER_COMMANDS = \
   infer-analyze \
   infer-capture \
   infer-compile \
+  infer-debug \
   infer-explore \
   infer-help \
   infer-report \
diff --git a/infer/man/man1/infer-debug.txt b/infer/man/man1/infer-debug.txt
new file mode 100644
index 000000000..381849994
--- /dev/null
+++ b/infer/man/man1/infer-debug.txt
@@ -0,0 +1,122 @@
+NAME
+       infer-debug - print internal infer data structures
+
+SYNOPSIS
+       infer debug --global-tenv
+       infer debug --procedures [options]
+       infer debug --source-files [options]
+
+
+DESCRIPTION
+       If --procedures is passed, print information about each procedures
+       captured by infer.
+
+       If --source-files is passed, print information about captured source
+       files.
+
+       If --global-tenv is passed, print the global type environment (if
+       any).
+
+       At least one of the above options must be passed.
+
+
+
+OPTIONS
+       --help
+           Show this manual
+
+       --help-format { auto | groff | pager | plain }
+           Show this help in the specified format. auto sets the format to
+           plain if the environment variable TERM is "dumb" or undefined, and
+           to pager otherwise.
+
+       --help-full
+           Show this manual with all internal options in the INTERNAL OPTIONS
+           section
+DEBUG GLOBAL TYPE ENVIRONMENT
+       --global-tenv
+           Activates: Print the global type environment. (Conversely:
+           --no-global-tenv)
+DEBUG PROCEDURES
+       --procedures
+           Activates: Print functions and methods discovered by infer
+           (Conversely: --no-procedures)
+
+       --procedures-attributes
+           Activates: Print the attributes of each procedure in the output of
+           --procedures (Conversely: --no-procedures-attributes)
+
+       --no-procedures-definedness
+           Deactivates: Include procedures definedness in the output of
+           --procedures, i.e. whether the procedure definition was found, or
+           only the procedure declaration, or the procedure is an
+           auto-generated Objective-C accessor (Conversely:
+           --procedures-definedness)
+
+       --procedures-filter filter
+           With --procedures, only print functions and methods (procedures)
+           matching the specified filter. A procedure filter is of the form
+           path_pattern:procedure_name. Patterns are interpreted as OCaml Str
+           regular expressions. For instance, to keep only methods named
+           "foo", one can use the filter ".*:foo", or "foo" for short.
+
+       --procedures-name
+           Activates: Include procedures names in the output of --procedures
+           (Conversely: --no-procedures-name)
+
+       --no-procedures-source-file
+           Deactivates: Include the source file in which the procedure
+           definition or declaration was found in the output of --procedures
+           (Conversely: --procedures-source-file)
+
+       --procedures-summary
+           Activates: Print the summaries of each procedure in the output of
+           --procedures (Conversely: --no-procedures-summary)
+DEBUG SOURCE FILES
+       --source-files
+           Activates: Print source files discovered by infer (Conversely:
+           --no-source-files)
+
+       --source-files-cfg
+           Activates: Output a dotty file in infer-out/captured for each
+           source file in the output of --source-files (Conversely:
+           --no-source-files-cfg)
+
+       --source-files-filter filter
+           With --source-files, only print source files matching the
+           specified filter. The filter is a pattern that should match the
+           file path. Patterns are interpreted as OCaml Str regular
+           expressions.
+
+       --source-files-freshly-captured
+           Activates: Print whether the source file has been captured in the
+           most recent capture phase in the output of --source-files.
+           (Conversely: --no-source-files-freshly-captured)
+
+       --source-files-procedure-names
+           Activates: Print the names of procedure of each source file in the
+           output of --source-files (Conversely:
+           --no-source-files-procedure-names)
+
+       --source-files-type-environment
+           Activates: Print the type environment of each source file in the
+           output of --source-files (Conversely:
+           --no-source-files-type-environment)
+
+
+ENVIRONMENT
+       INFER_ARGS, INFERCONFIG, INFER_STRICT_MODE
+           See the ENVIRONMENT section in the manual of infer(1).
+
+FILES
+       .inferconfig
+           See the FILES section in the manual of infer(1).
+
+
+
+
+SEE ALSO
+       infer-explore(1), infer-report(1)
+
+
+
diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt
index 38c30102b..bce669ddb 100644
--- a/infer/man/man1/infer-explore.txt
+++ b/infer/man/man1/infer-explore.txt
@@ -3,20 +3,12 @@ NAME
 
 SYNOPSIS
        infer explore [options]
-       infer explore --procedures [options]
-       infer explore --source-files [options]
 
 
 DESCRIPTION
-       If --procedures is passed, print information about each procedure
-       captured by infer.
-
-       If --source-files is passed, print information about captured source
-       files.
-
-       Otherwise, show the list of bugs on the console and explore symbolic
-       program traces emitted by infer to explain a report. Can also generate
-       an HTML report from a JSON report.
+       Show the list of bugs on the console and explore symbolic program
+       traces emitted by infer to explain a report. Can also generate an HTML
+       report from a JSON report.
 
 
 
@@ -50,71 +42,6 @@ EXPLORE BUGS
        --no-source-preview
            Deactivates: print code excerpts around trace elements
            (Conversely: --source-preview)
-EXPLORE PROCEDURES
-       --procedures
-           Activates: Print functions and methods discovered by infer
-           (Conversely: --no-procedures)
-
-       --procedures-attributes
-           Activates: Print the attributes of each procedure in the output of
-           --procedures (Conversely: --no-procedures-attributes)
-
-       --no-procedures-definedness
-           Deactivates: Include procedures definedness in the output of
-           --procedures, i.e. whether the procedure definition was found, or
-           only the procedure declaration, or the procedure is an
-           auto-generated Objective-C accessor (Conversely:
-           --procedures-definedness)
-
-       --procedures-filter filter
-           With --procedures, only print functions and methods (procedures)
-           matching the specified filter. A procedure filter is of the form
-           path_pattern:procedure_name. Patterns are interpreted as OCaml Str
-           regular expressions. For instance, to keep only methods named
-           "foo", one can use the filter ".*:foo", or "foo" for short.
-
-       --procedures-name
-           Activates: Include procedures names in the output of --procedures
-           (Conversely: --no-procedures-name)
-
-       --no-procedures-source-file
-           Deactivates: Include the source file in which the procedure
-           definition or declaration was found in the output of --procedures
-           (Conversely: --procedures-source-file)
-
-       --procedures-summary
-           Activates: Print the summaries of each procedure in the output of
-           --procedures (Conversely: --no-procedures-summary)
-EXPLORE SOURCE FILES
-       --source-files
-           Activates: Print source files discovered by infer (Conversely:
-           --no-source-files)
-
-       --source-files-cfg
-           Activates: Output a dotty file in infer-out/captured for each
-           source file in the output of --source-files (Conversely:
-           --no-source-files-cfg)
-
-       --source-files-filter filter
-           With --source-files, only print source files matching the
-           specified filter. The filter is a pattern that should match the
-           file path. Patterns are interpreted as OCaml Str regular
-           expressions.
-
-       --source-files-freshly-captured
-           Activates: Print whether the source file has been captured in the
-           most recent capture phase in the output of --source-files.
-           (Conversely: --no-source-files-freshly-captured)
-
-       --source-files-procedure-names
-           Activates: Print the names of procedure of each source file in the
-           output of --source-files (Conversely:
-           --no-source-files-procedure-names)
-
-       --source-files-type-environment
-           Activates: Print the type environment of each source file in the
-           output of --source-files (Conversely:
-           --no-source-files-type-environment)
 
 
 ENVIRONMENT
diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 81244270e..20d9351fc 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -582,13 +582,17 @@ OPTIONS
        --generated-classes path
            Specify where to load the generated class files           See also infer-capture(1).
 
+       --global-tenv
+           Activates: Print the global type environment. (Conversely:
+           --no-global-tenv)           See also infer-debug(1).
+
        --headers
            Activates: Analyze code in header files (Conversely: --no-headers)       
     See also infer-capture(1).
 
        --help
            Show this manual           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-checker +checker-id
@@ -599,13 +603,13 @@ OPTIONS
            Show this help in the specified format. auto sets the format to
            plain if the environment variable TERM is "dumb" or undefined, and
            to pager otherwise.           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-full
            Show this manual with all internal options in the INTERNAL OPTIONS
            section           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-issue-type +UNIQUE_ID
@@ -813,19 +817,19 @@ OPTIONS
 
        --procedures
            Activates: Print functions and methods discovered by infer
-           (Conversely: --no-procedures)           See also infer-explore(1).
+           (Conversely: --no-procedures)           See also infer-debug(1).
 
        --procedures-attributes
            Activates: Print the attributes of each procedure in the output of
            --procedures (Conversely: --no-procedures-attributes)       
-    See also infer-explore(1).
+    See also infer-debug(1).
 
        --no-procedures-definedness
            Deactivates: Include procedures definedness in the output of
            --procedures, i.e. whether the procedure definition was found, or
            only the procedure declaration, or the procedure is an
            auto-generated Objective-C accessor (Conversely:
-           --procedures-definedness)           See also infer-explore(1).
+           --procedures-definedness)           See also infer-debug(1).
 
        --procedures-filter filter
            With --procedures, only print functions and methods (procedures)
@@ -833,20 +837,20 @@ OPTIONS
            path_pattern:procedure_name. Patterns are interpreted as OCaml Str
            regular expressions. For instance, to keep only methods named
            "foo", one can use the filter ".*:foo", or "foo" for short.       
-    See also infer-explore(1).
+    See also infer-debug(1).
 
        --procedures-name
            Activates: Include procedures names in the output of --procedures
-           (Conversely: --no-procedures-name)           See also infer-explore(1).
+           (Conversely: --no-procedures-name)           See also infer-debug(1).
 
        --no-procedures-source-file
            Deactivates: Include the source file in which the procedure
            definition or declaration was found in the output of --procedures
-           (Conversely: --procedures-source-file)           See also infer-explore(1).
+           (Conversely: --procedures-source-file)           See also infer-debug(1).
 
        --procedures-summary
            Activates: Print the summaries of each procedure in the output of
-           --procedures (Conversely: --no-procedures-summary)           See also infer-explore(1).
+           --procedures (Conversely: --no-procedures-summary)           See also infer-debug(1).
 
        --no-progress-bar,-P
            Deactivates: Show a progress bar (Conversely: --progress-bar | -p)       
@@ -1043,33 +1047,33 @@ OPTIONS
 
        --source-files
            Activates: Print source files discovered by infer (Conversely:
-           --no-source-files)           See also infer-explore(1).
+           --no-source-files)           See also infer-debug(1).
 
        --source-files-cfg
            Activates: Output a dotty file in infer-out/captured for each
            source file in the output of --source-files (Conversely:
-           --no-source-files-cfg)           See also infer-explore(1).
+           --no-source-files-cfg)           See also infer-debug(1).
 
        --source-files-filter filter
            With --source-files, only print source files matching the
            specified filter. The filter is a pattern that should match the
            file path. Patterns are interpreted as OCaml Str regular
-           expressions.           See also infer-explore(1).
+           expressions.           See also infer-debug(1).
 
        --source-files-freshly-captured
            Activates: Print whether the source file has been captured in the
            most recent capture phase in the output of --source-files.
-           (Conversely: --no-source-files-freshly-captured)           See also infer-explore(1).
+           (Conversely: --no-source-files-freshly-captured)           See also infer-debug(1).
 
        --source-files-procedure-names
            Activates: Print the names of procedure of each source file in the
            output of --source-files (Conversely:
-           --no-source-files-procedure-names)           See also infer-explore(1).
+           --no-source-files-procedure-names)           See also infer-debug(1).
 
        --source-files-type-environment
            Activates: Print the type environment of each source file in the
            output of --source-files (Conversely:
-           --no-source-files-type-environment)           See also infer-explore(1).
+           --no-source-files-type-environment)           See also infer-debug(1).
 
        --no-source-preview
            Deactivates: print code excerpts around trace elements
@@ -1960,7 +1964,7 @@ FILES
 
 
 SEE ALSO
-       infer-analyze(1), infer-capture(1), infer-compile(1),
+       infer-analyze(1), infer-capture(1), infer-compile(1), infer-debug(1),
        infer-explore(1), infer-help(1), infer-report(1), infer-reportdiff(1),
        infer-run(1)
 
diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt
index 54c619ef7..c134b3c4a 100644
--- a/infer/man/man1/infer.txt
+++ b/infer/man/man1/infer.txt
@@ -582,13 +582,17 @@ OPTIONS
        --generated-classes path
            Specify where to load the generated class files           See also infer-capture(1).
 
+       --global-tenv
+           Activates: Print the global type environment. (Conversely:
+           --no-global-tenv)           See also infer-debug(1).
+
        --headers
            Activates: Analyze code in header files (Conversely: --no-headers)       
     See also infer-capture(1).
 
        --help
            Show this manual           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-checker +checker-id
@@ -599,13 +603,13 @@ OPTIONS
            Show this help in the specified format. auto sets the format to
            plain if the environment variable TERM is "dumb" or undefined, and
            to pager otherwise.           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-full
            Show this manual with all internal options in the INTERNAL OPTIONS
            section           See also infer-analyze(1), infer-capture(1), infer-compile(1),
-           infer-explore(1), infer-help(1), infer-report(1),
+           infer-debug(1), infer-explore(1), infer-help(1), infer-report(1),
            infer-reportdiff(1), and infer-run(1).
 
        --help-issue-type +UNIQUE_ID
@@ -813,19 +817,19 @@ OPTIONS
 
        --procedures
            Activates: Print functions and methods discovered by infer
-           (Conversely: --no-procedures)           See also infer-explore(1).
+           (Conversely: --no-procedures)           See also infer-debug(1).
 
        --procedures-attributes
            Activates: Print the attributes of each procedure in the output of
            --procedures (Conversely: --no-procedures-attributes)       
-    See also infer-explore(1).
+    See also infer-debug(1).
 
        --no-procedures-definedness
            Deactivates: Include procedures definedness in the output of
            --procedures, i.e. whether the procedure definition was found, or
            only the procedure declaration, or the procedure is an
            auto-generated Objective-C accessor (Conversely:
-           --procedures-definedness)           See also infer-explore(1).
+           --procedures-definedness)           See also infer-debug(1).
 
        --procedures-filter filter
            With --procedures, only print functions and methods (procedures)
@@ -833,20 +837,20 @@ OPTIONS
            path_pattern:procedure_name. Patterns are interpreted as OCaml Str
            regular expressions. For instance, to keep only methods named
            "foo", one can use the filter ".*:foo", or "foo" for short.       
-    See also infer-explore(1).
+    See also infer-debug(1).
 
        --procedures-name
            Activates: Include procedures names in the output of --procedures
-           (Conversely: --no-procedures-name)           See also infer-explore(1).
+           (Conversely: --no-procedures-name)           See also infer-debug(1).
 
        --no-procedures-source-file
            Deactivates: Include the source file in which the procedure
            definition or declaration was found in the output of --procedures
-           (Conversely: --procedures-source-file)           See also infer-explore(1).
+           (Conversely: --procedures-source-file)           See also infer-debug(1).
 
        --procedures-summary
            Activates: Print the summaries of each procedure in the output of
-           --procedures (Conversely: --no-procedures-summary)           See also infer-explore(1).
+           --procedures (Conversely: --no-procedures-summary)           See also infer-debug(1).
 
        --no-progress-bar,-P
            Deactivates: Show a progress bar (Conversely: --progress-bar | -p)       
@@ -1043,33 +1047,33 @@ OPTIONS
 
        --source-files
            Activates: Print source files discovered by infer (Conversely:
-           --no-source-files)           See also infer-explore(1).
+           --no-source-files)           See also infer-debug(1).
 
        --source-files-cfg
            Activates: Output a dotty file in infer-out/captured for each
            source file in the output of --source-files (Conversely:
-           --no-source-files-cfg)           See also infer-explore(1).
+           --no-source-files-cfg)           See also infer-debug(1).
 
        --source-files-filter filter
            With --source-files, only print source files matching the
            specified filter. The filter is a pattern that should match the
            file path. Patterns are interpreted as OCaml Str regular
-           expressions.           See also infer-explore(1).
+           expressions.           See also infer-debug(1).
 
        --source-files-freshly-captured
            Activates: Print whether the source file has been captured in the
            most recent capture phase in the output of --source-files.
-           (Conversely: --no-source-files-freshly-captured)           See also infer-explore(1).
+           (Conversely: --no-source-files-freshly-captured)           See also infer-debug(1).
 
        --source-files-procedure-names
            Activates: Print the names of procedure of each source file in the
            output of --source-files (Conversely:
-           --no-source-files-procedure-names)           See also infer-explore(1).
+           --no-source-files-procedure-names)           See also infer-debug(1).
 
        --source-files-type-environment
            Activates: Print the type environment of each source file in the
            output of --source-files (Conversely:
-           --no-source-files-type-environment)           See also infer-explore(1).
+           --no-source-files-type-environment)           See also infer-debug(1).
 
        --no-source-preview
            Deactivates: print code excerpts around trace elements
@@ -1204,7 +1208,7 @@ FILES
 
 
 SEE ALSO
-       infer-analyze(1), infer-capture(1), infer-compile(1),
+       infer-analyze(1), infer-capture(1), infer-compile(1), infer-debug(1),
        infer-explore(1), infer-help(1), infer-report(1), infer-reportdiff(1),
        infer-run(1)
 
diff --git a/infer/src/IR/Struct.ml b/infer/src/IR/Struct.ml
index 217061f1c..e2dbb356d 100644
--- a/infer/src/IR/Struct.ml
+++ b/infer/src/IR/Struct.ml
@@ -39,30 +39,32 @@ let pp_field pe f (field_name, typ, ann) =
 
 
 let pp pe name f {fields; supers; methods; exported_objc_methods; annots} =
-  if Config.debug_mode then
-    (* change false to true to print the details of struct *)
-    F.fprintf f
-      "%a @\n\
-       \tfields: {%a@\n\
-       \t}@\n\
-       \tsupers: {%a@\n\
-       \t}@\n\
-       \tmethods: {%a@\n\
-       \t}@\n\
-       \texported_obj_methods: {%a@\n\
-       \t}@\n\
-       \tannots: {%a@\n\
-       \t}"
-      Typ.Name.pp name
-      (Pp.seq (pp_field pe))
-      fields
-      (Pp.seq (fun f n -> F.fprintf f "@\n\t\t%a" Typ.Name.pp n))
-      supers
-      (Pp.seq (fun f m -> F.fprintf f "@\n\t\t%a" Procname.pp m))
-      methods
-      (Pp.seq (fun f m -> F.fprintf f "@\n\t\t%a" Procname.pp m))
-      exported_objc_methods Annot.Item.pp annots
-  else Typ.Name.pp f name
+  let pp_field pe f (field_name, typ, ann) =
+    F.fprintf f "@;<0 2>%a %a %a" (Typ.pp_full pe) typ Fieldname.pp field_name Annot.Item.pp ann
+  in
+  let seq pp fmt = function
+    | [] ->
+        ()
+    | lst ->
+        Pp.seq pp fmt lst ;
+        F.pp_print_break fmt 0 0
+  in
+  F.fprintf f
+    "%a@,\
+     @[<v>fields: {@[<v>%a@]}@,\
+     supers: {@[<v>%a@]}@,\
+     methods: {@[<v>%a@]}@,\
+     exported_obj_methods: {@[<v>%a@]}@,\
+     annots: {%a}@]@,"
+    Typ.Name.pp name
+    (seq (pp_field pe))
+    fields
+    (seq (fun f n -> F.fprintf f "@;<0 2>%a" Typ.Name.pp n))
+    supers
+    (seq (fun f m -> F.fprintf f "@;<0 2>%a" Procname.pp m))
+    methods
+    (seq (fun f m -> F.fprintf f "@;<0 2>%a" Procname.pp m))
+    exported_objc_methods Annot.Item.pp annots
 
 
 let internal_mk_struct ?default ?fields ?statics ?methods ?exported_objc_methods ?supers ?annots
diff --git a/infer/src/IR/Tenv.ml b/infer/src/IR/Tenv.ml
index 5d0901c1c..84e127539 100644
--- a/infer/src/IR/Tenv.ml
+++ b/infer/src/IR/Tenv.ml
@@ -18,11 +18,7 @@ module TypenameHashNormalizer = MaximumSharing.ForHashtbl (TypenameHash)
 type t = Struct.t TypenameHash.t
 
 let pp fmt (tenv : t) =
-  TypenameHash.iter
-    (fun name typ ->
-      Format.fprintf fmt "@[<6>NAME: %s@]@," (Typ.Name.to_string name) ;
-      Format.fprintf fmt "@[<6>TYPE: %a@]@," (Struct.pp Pp.text name) typ )
-    tenv
+  TypenameHash.iter (fun name typ -> Format.fprintf fmt "%a@," (Struct.pp Pp.text name) typ) tenv
 
 
 (** Create a new type environment. *)
diff --git a/infer/src/IR/Tenv.mli b/infer/src/IR/Tenv.mli
index 02ce81dea..8b4e4fd86 100644
--- a/infer/src/IR/Tenv.mli
+++ b/infer/src/IR/Tenv.mli
@@ -50,13 +50,12 @@ val mk_struct :
 val add_field : t -> Typ.Name.t -> Struct.field -> unit
 (** Add a field to a given struct in the global type environment. *)
 
-val pp : Format.formatter -> t -> unit [@@warning "-32"]
+val pp : Format.formatter -> t -> unit
 (** print a type environment *)
 
 type per_file = Global | FileLocal of t
 
 val pp_per_file : Format.formatter -> per_file -> unit
-  [@@warning "-32"]
 (** print per file type environment *)
 
 val merge : src:t -> dst:t -> unit
diff --git a/infer/src/atd/InferCommand.ml b/infer/src/atd/InferCommand.ml
index 0a86c6442..b578799ba 100644
--- a/infer/src/atd/InferCommand.ml
+++ b/infer/src/atd/InferCommand.ml
@@ -7,7 +7,7 @@
 open Core
 
 (* NOTE: All variants must be also added to [command_to_string] below *)
-type t = Analyze | Capture | Compile | Explore | Help | Report | ReportDiff | Run
+type t = Analyze | Capture | Compile | Debug | Explore | Help | Report | ReportDiff | Run
 [@@deriving compare]
 
 let equal = [%compare.equal: t]
@@ -16,6 +16,7 @@ let command_to_string =
   [ (Analyze, "analyze")
   ; (Capture, "capture")
   ; (Compile, "compile")
+  ; (Debug, "debug")
   ; (Explore, "explore")
   ; (Help, "help")
   ; (Report, "report")
diff --git a/infer/src/atd/InferCommand.mli b/infer/src/atd/InferCommand.mli
index ac7039886..e1a6a8643 100644
--- a/infer/src/atd/InferCommand.mli
+++ b/infer/src/atd/InferCommand.mli
@@ -13,6 +13,7 @@ type t =
   | Compile
       (** set up the infer environment then run the compilation commands without capturing the
           source files *)
+  | Debug  (** print information about internal structures *)
   | Explore  (** explore infer reports *)
   | Help  (** documentation about various aspects of infer *)
   | Report  (** post-process infer results and reports *)
diff --git a/infer/src/base/CommandDoc.ml b/infer/src/base/CommandDoc.ml
index b26cd08b8..7af2ec00d 100644
--- a/infer/src/base/CommandDoc.ml
+++ b/infer/src/base/CommandDoc.ml
@@ -116,22 +116,30 @@ let compile =
     ~see_also:InferCommand.[Capture]
 
 
-let explore =
-  mk_command_doc ~title:"Infer Explore"
-    ~short_description:"explore the error traces in infer reports"
+let debug =
+  mk_command_doc ~title:"Infer Debug" ~short_description:"print internal infer data structures"
     ~synopsis:
-      {|$(b,infer) $(b,explore) $(i,[options])
-$(b,infer) $(b,explore) $(b,--procedures) $(i,[options])
-$(b,infer) $(b,explore) $(b,--source-files) $(i,[options])|}
+      {|$(b,infer) $(b,debug) $(b,--global-tenv)
+$(b,infer) $(b,debug) $(b,--procedures) $(i,[options])
+$(b,infer) $(b,debug) $(b,--source-files) $(i,[options])|}
     ~description:
       [ `P
-          "If $(b,--procedures) is passed, print information about each procedure captured by \
+          "If $(b,--procedures) is passed, print information about each procedures captured by \
            infer."
       ; `P "If $(b,--source-files) is passed, print information about captured source files."
-      ; `P
-          "Otherwise, show the list of bugs on the console and explore symbolic program traces \
-           emitted by infer to explain a report. Can also generate an HTML report from a JSON \
-           report." ]
+      ; `P "If $(b,--global-tenv) is passed,  print the global type environment (if any)."
+      ; `P "At least one of the above options must be passed." ]
+    ~see_also:InferCommand.[Explore; Report]
+
+
+let explore =
+  mk_command_doc ~title:"Infer Explore"
+    ~short_description:"explore the error traces in infer reports"
+    ~synopsis:{|$(b,infer) $(b,explore) $(i,[options])|}
+    ~description:
+      [ `P
+          "Show the list of bugs on the console and explore symbolic program traces emitted by \
+           infer to explain a report. Can also generate an HTML report from a JSON report." ]
     ~see_also:InferCommand.[Report; Run]
 
 
@@ -326,6 +334,7 @@ let command_to_data =
   [ mk Analyze analyze
   ; mk Capture capture
   ; mk Compile compile
+  ; mk Debug debug
   ; mk Explore explore
   ; mk Help help
   ; mk Report report
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 14cdfc6c8..4a42052b8 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -139,9 +139,11 @@ let manual_clang_linters = "CLANG LINTERS OPTIONS"
 
 let manual_explore_bugs = "EXPLORE BUGS"
 
-let manual_explore_procedures = "EXPLORE PROCEDURES"
+let manual_debug_procedures = "DEBUG PROCEDURES"
 
-let manual_explore_source_files = "EXPLORE SOURCE FILES"
+let manual_debug_source_files = "DEBUG SOURCE FILES"
+
+let manual_debug_global_tenv = "DEBUG GLOBAL TYPE ENVIRONMENT"
 
 let manual_generic = Cmdliner.Manpage.s_options
 
@@ -485,7 +487,7 @@ let () =
     match cmd with
     | Report ->
         `Add
-    | Analyze | Capture | Compile | Explore | Help | ReportDiff | Run ->
+    | Analyze | Capture | Compile | Debug | Explore | Help | ReportDiff | Run ->
         `Reject
   in
   (* make sure we generate doc for all the commands we know about *)
@@ -985,7 +987,7 @@ and ( bo_debug
   let all_generic_manuals =
     List.filter_map InferCommand.all_commands ~f:(fun (command : InferCommand.t) ->
         match command with
-        | Explore | Help ->
+        | Debug | Explore | Help ->
             None
         | (Analyze | Capture | Compile | Report | ReportDiff | Run) as command ->
             Some (command, manual_generic) )
@@ -1700,6 +1702,11 @@ and _print_log_identifier =
     "[DOES NOTHING] Print the unique identifier that is common to all logged events"
 
 
+and global_tenv =
+  CLOpt.mk_bool ~long:"global-tenv" "Print the global type environment."
+    ~in_help:InferCommand.[(Debug, manual_debug_global_tenv)]
+
+
 and print_using_diff =
   CLOpt.mk_bool ~deprecated_no:["noprintdiff"] ~long:"print-using-diff" ~default:true
     "Highlight the difference w.r.t. the previous prop when printing symbolic execution debug info"
@@ -1707,19 +1714,19 @@ and print_using_diff =
 
 and procedures =
   CLOpt.mk_bool ~long:"procedures"
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Print functions and methods discovered by infer"
 
 
 and procedures_attributes =
   CLOpt.mk_bool ~long:"procedures-attributes"
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Print the attributes of each procedure in the output of $(b,--procedures)"
 
 
 and procedures_definedness =
   CLOpt.mk_bool ~long:"procedures-definedness" ~default:true
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Include procedures definedness in the output of $(b,--procedures), i.e. whether the procedure \
      definition was found, or only the procedure declaration, or the procedure is an \
      auto-generated Objective-C accessor"
@@ -1727,7 +1734,7 @@ and procedures_definedness =
 
 and procedures_filter =
   CLOpt.mk_string_opt ~long:"procedures-filter" ~meta:"filter"
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "With $(b,--procedures), only print functions and methods (procedures) matching the specified \
      $(i,filter). A procedure filter is of the form $(i,path_pattern:procedure_name). Patterns are \
      interpreted as OCaml Str regular expressions. For instance, to keep only methods named \
@@ -1736,20 +1743,20 @@ and procedures_filter =
 
 and procedures_name =
   CLOpt.mk_bool ~long:"procedures-name"
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Include procedures names in the output of $(b,--procedures)"
 
 
 and procedures_source_file =
   CLOpt.mk_bool ~long:"procedures-source-file" ~default:true
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Include the source file in which the procedure definition or declaration was found in the \
      output of $(b,--procedures)"
 
 
 and procedures_summary =
   CLOpt.mk_bool ~long:"procedures-summary" ~default:false
-    ~in_help:InferCommand.[(Explore, manual_explore_procedures)]
+    ~in_help:InferCommand.[(Debug, manual_debug_procedures)]
     "Print the summaries of each procedure in the output of $(b,--procedures)"
 
 
@@ -2077,13 +2084,13 @@ and source_preview =
 
 and source_files =
   CLOpt.mk_bool ~long:"source-files"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     "Print source files discovered by infer"
 
 
 and source_files_cfg =
   CLOpt.mk_bool ~long:"source-files-cfg"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     (Printf.sprintf
        "Output a dotty file in %s for each source file in the output of $(b,--source-files)"
        (ResultsDirEntryName.get_path ~results_dir:"infer-out" Debug))
@@ -2091,7 +2098,7 @@ and source_files_cfg =
 
 and source_files_filter =
   CLOpt.mk_string_opt ~long:"source-files-filter" ~meta:"filter"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     "With $(b,--source-files), only print source files matching the specified $(i,filter). The \
      filter is a pattern that should match the file path. Patterns are interpreted as OCaml Str \
      regular expressions."
@@ -2099,19 +2106,19 @@ and source_files_filter =
 
 and source_files_type_environment =
   CLOpt.mk_bool ~long:"source-files-type-environment"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     "Print the type environment of each source file in the output of $(b,--source-files)"
 
 
 and source_files_procedure_names =
   CLOpt.mk_bool ~long:"source-files-procedure-names"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     "Print the names of procedure of each source file in the output of $(b,--source-files)"
 
 
 and source_files_freshly_captured =
   CLOpt.mk_bool ~long:"source-files-freshly-captured"
-    ~in_help:InferCommand.[(Explore, manual_explore_source_files)]
+    ~in_help:InferCommand.[(Debug, manual_debug_source_files)]
     "Print whether the source file has been captured in the most recent capture phase in the \
      output of $(b,--source-files)."
 
@@ -2787,6 +2794,8 @@ and html = !html
 
 and hoisting_report_only_expensive = !hoisting_report_only_expensive
 
+and global_tenv = !global_tenv
+
 and icfg_dotty_outfile = !icfg_dotty_outfile
 
 and inclusive_cost = !inclusive_cost
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 0461d0b9f..6cddfffcb 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -312,6 +312,8 @@ val hoisting_report_only_expensive : bool
 
 val html : bool
 
+val global_tenv : bool
+
 val icfg_dotty_outfile : string option
 
 val infer_is_clang : bool
diff --git a/infer/src/infer.ml b/infer/src/infer.ml
index 81353195c..567b781c9 100644
--- a/infer/src/infer.ml
+++ b/infer/src/infer.ml
@@ -61,11 +61,13 @@ let setup () =
         SourceFiles.mark_all_stale () )
   | Explore ->
       ResultsDir.assert_results_dir "please run an infer analysis first"
+  | Debug ->
+      ResultsDir.assert_results_dir "please run an infer analysis or capture first"
   | Help ->
       () ) ;
   let has_result_dir =
     match Config.command with
-    | Analyze | Capture | Compile | Explore | Report | ReportDiff | Run ->
+    | Analyze | Capture | Compile | Debug | Explore | Report | ReportDiff | Run ->
         true
     | Help ->
         false
@@ -209,9 +211,17 @@ let () =
       ReportDiff.reportdiff ~current_report:Config.report_current
         ~previous_report:Config.report_previous ~current_costs:Config.costs_current
         ~previous_costs:Config.costs_previous
-  | Explore -> (
-    match (Config.procedures, Config.source_files) with
-    | true, false ->
+  | Debug when not Config.(global_tenv || procedures || source_files) ->
+      L.die UserError
+        "Expected at least one of '--procedures', '--source_files', or '--global-tenv'"
+  | Debug ->
+      ( if Config.global_tenv then
+        match Tenv.load_global () with
+        | None ->
+            L.result "No global type environment was found.@."
+        | Some tenv ->
+            L.result "Global type environment:@\n@[<v>%a@]" Tenv.pp tenv ) ;
+      ( if Config.procedures then
         let filter = Lazy.force Filtering.procedures_filter in
         if Config.procedures_summary then
           let pp_summary fmt proc_name =
@@ -228,8 +238,8 @@ let () =
             Config.(
               Procedures.pp_all ~filter ~proc_name:procedures_name ~attr_kind:procedures_definedness
                 ~source_file:procedures_source_file ~proc_attributes:procedures_attributes)
-            ()
-    | false, true ->
+            () ) ;
+      if Config.source_files then (
         let filter = Lazy.force Filtering.source_files_filter in
         L.result "%a"
           (SourceFiles.pp_all ~filter ~type_environment:Config.source_files_type_environment
@@ -250,18 +260,16 @@ let () =
               (* emit the dot file in captured/... *)
               DotCfg.emit_frontend_cfg source_file cfgs ) ;
           L.result "CFGs written in %s/*/%s@." (ResultsDir.get_path Debug)
-            Config.dotty_frontend_output )
-    | false, false ->
-        (* explore bug traces *)
-        if Config.html then
-          TraceBugs.gen_html_report ~report_json:(ResultsDir.get_path ReportJson)
-            ~show_source_context:Config.source_preview ~max_nested_level:Config.max_nesting
-            ~report_html_dir:(ResultsDir.get_path ReportHtml)
-        else
-          TraceBugs.explore ~selector_limit:None ~report_json:(ResultsDir.get_path ReportJson)
-            ~report_txt:(ResultsDir.get_path ReportText) ~selected:Config.select
-            ~show_source_context:Config.source_preview ~max_nested_level:Config.max_nesting
-    | true, true ->
-        L.user_error "Options --procedures and --source-files cannot be used together.@\n" ) ) ;
+            Config.dotty_frontend_output ) )
+  | Explore ->
+      if (* explore bug traces *)
+         Config.html then
+        TraceBugs.gen_html_report ~report_json:(ResultsDir.get_path ReportJson)
+          ~show_source_context:Config.source_preview ~max_nested_level:Config.max_nesting
+          ~report_html_dir:(ResultsDir.get_path ReportHtml)
+      else
+        TraceBugs.explore ~selector_limit:None ~report_json:(ResultsDir.get_path ReportJson)
+          ~report_txt:(ResultsDir.get_path ReportText) ~selected:Config.select
+          ~show_source_context:Config.source_preview ~max_nested_level:Config.max_nesting ) ;
   (* to make sure the exitcode=0 case is logged, explicitly invoke exit *)
   L.exit 0
diff --git a/infer/src/integration/Driver.ml b/infer/src/integration/Driver.ml
index ad532e929..cdacbbfcb 100644
--- a/infer/src/integration/Driver.ml
+++ b/infer/src/integration/Driver.ml
@@ -242,7 +242,7 @@ let analyze_and_report ?suppress_console_report ~changed_files mode =
     | _ when Config.infer_is_clang || Config.infer_is_javac ->
         (* Called from another integration to do capture only. *)
         (false, false)
-    | (Capture | Compile | Explore | Help | Report | ReportDiff), _ ->
+    | (Capture | Compile | Debug | Explore | Help | Report | ReportDiff), _ ->
         (false, false)
     | (Analyze | Run), _ ->
         (true, true)