Bring back context printing in checker

3 files changed, 12 insertions, 29 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 588fb8e8b1..57adc79475 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -8,12 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*
 open Pp
 open Names
 open Declarations
 open Environ
-   *)
 
 let memory_stat = ref false
 
@@ -26,45 +24,32 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-(*
-let pr_engagement impr_set =
+let pr_engagement env =
   begin
-    match impr_set with
+    match engagement env with
     | ImpredicativeSet -> str "Theory: Set is impredicative"
     | PredicativeSet -> str "Theory: Set is predicative"
   end
 
-let cst_filter f csts =
-  Cmap_env.fold
-    (fun c ce acc -> if f c ce then c::acc else acc)
-    csts []
-
 let is_ax _ cb = not (Declareops.constant_has_body cb)
 
-let pr_ax csts =
-  let axs = cst_filter is_ax csts in
+let pr_ax env =
+  let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
   if axs = [] then
     str "Axioms: <none>"
   else
     hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
-      *)
 
-let print_context env = () (* FIXME
+let print_context env =
   if !output_context then begin
-    let
-      {env_globals=
-        {env_constants=csts; env_inductives=inds;
-         env_modules=mods; env_modtypes=mtys};
-       env_stratification=
-        {env_universes=univ; env_engagement=engt}} = env in
     Feedback.msg_notice
       (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
-      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax csts)));
-  end *)
+      str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_ax env)));
+  end
 
-let stats senv =
-  print_context senv;
+let stats env =
+  print_context env;
   print_memory_stat ()
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 0cda7f0c8a..b094da1c44 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -7,9 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-open Safe_typing
-
 val memory_stat : bool ref
 val output_context : bool ref
 
-val stats : safe_environment -> unit
+val stats : Environ.env -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index 06c1e053d5..346ae5fffb 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -395,5 +395,5 @@ let run senv =
 let start () =
   let senv = init() in
   let senv = run senv in
-  Check_stat.stats senv;
+  Check_stat.stats (Safe_typing.env_of_safe_env senv);
   exit 0