From e457ababc4cb5b75540cfa131a30fdee3f9bc0ed Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 10:20:23 +0000
Subject: [PATCH] logger added

---
 .../components/ng_kernel/nCicTypeChecker.ml   | 21 ++++++++++++-------
 .../components/ng_kernel/nCicTypeChecker.mli  |  3 +++
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index e6a5cbbc2..96b2f9186 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -11,6 +11,14 @@
 
 (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
 
+(* web interface stuff *)
+
+let logger = 
+  ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
@@ -1124,13 +1132,12 @@ and returns_a_coinductive ~subst context ty =
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
-and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
-(* ALIAS typecheck *)
-(*
-  let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
+and type_of_constant ref = 
+assert false        (*
+  let cobj =
+   match E.get_obj uri with
+   | true, cobj -> cobj
+   | false, uobj ->
          logger#log (`Start_type_checking uri) ;
          let ugraph1_dust =
           typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 51aa6458d..c333430b9 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -34,3 +34,6 @@ val typeof:
   NCic.context -> NCic.term -> 
     NCic.term
 
+val set_logger: 
+  ([ `Start_type_checking of NUri.uri 
+   | `Type_checking_completed of NUri.uri ] -> unit) -> unit
-- 
2.39.2