X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=96b2f9186fcc7ebfcec7714e9a35f6d1fe66df0a;hb=e457ababc4cb5b75540cfa131a30fdee3f9bc0ed;hp=5e4000740e44abf518f711def15996085e0545f1;hpb=a2b79ad8b6fdbe07ea9d92102b0764ac4004a6db;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 5e4000740..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
 
@@ -887,10 +895,10 @@ let rec typeof ~subst ~metasenv context term =
               let type_t = typeof_aux context t in
               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
                 raise (TypeCheckerFailure 
-                  (lazy (Printf.sprintf 
-                   ("Not well typed metavariable local context: "^^
-                    "expected a term of type %s, found %s of type %s") 
-                    (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+                 (lazy (Printf.sprintf 
+                  ("Not well typed metavariable local context: "^^
+                  "expected a term of type %s, found %s of type %s") 
+                  (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
         ) l lifted_canonical_context 
        with
         Invalid_argument _ ->
@@ -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