X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicLogger.mli;h=408bc8879998f0da714948589b3b441dc3425460;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=848b30573cce84d618929e1f1db4ddb81a670df8;hpb=98295941bee765a0cb4070eb3f2df553228c11c8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicLogger.mli b/helm/ocaml/cic_proof_checking/cicLogger.mli
index 848b30573..408bc8879 100644
--- a/helm/ocaml/cic_proof_checking/cicLogger.mli
+++ b/helm/ocaml/cic_proof_checking/cicLogger.mli
@@ -29,5 +29,14 @@ type msg =
  | `Trusting of UriManager.uri
  ]
 
+  (** Stateless logging. Each message is logged with indentation level 1 *)
 val log: msg -> unit
 
+  (** Stateful logging. Each `Start_type_checing message increase the
+  * indentation level by 1, each `Type_checking_completed message decrease it by
+  * the same amount. *)
+class logger:
+  object
+    method log: msg -> unit
+  end
+