]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
New cool "type-checking" notation using colors and non-linear patterns.
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index f7839a6f9c939fa59c7b56d391b1e148bcb430dc..dc2bfee9334bc4966ed8f2661e22dbcbb05af290 100644 (file)
@@ -44,8 +44,11 @@ let main =
       if !summary > 1 then
         AO.count (AO.print_counters Cps.id) AO.initial_counters book;
       let f env =
-         if !summary > 1 then
-           MO.count (MO.print_counters Cps.id) MO.initial_counters env
+        if !summary > 1 then
+           MO.count (MO.print_counters Cps.id) MO.initial_counters env;
+         let frm = Format.err_formatter in
+         Format.pp_set_margin frm max_int;
+         MO.pp_environment Cps.id frm (List.rev env)
       in
       if !stage > 0 then MA.meta_of_aut f book
    in