renamed module "logger" to "cicLogger" to avoid confusion with user

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 7521f0f90b0456ca0ec8c0bf4c4e9a2d18922c25..0d171604d74beed6e5ce8c1ce3a6f000d457f772 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -136,7 +136,7 @@ let rec type_of_constant uri =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Constant (_,Some te,ty,_) ->
@@ -166,7 +166,7 @@ let rec type_of_constant uri =
            raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri)))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -184,7 +184,7 @@ and type_of_variable uri =
   match CicEnvironment.is_type_checked ~trust:true uri with
      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
-      Logger.log (`Start_type_checking uri) ;
+      CicLogger.log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -196,7 +196,7 @@ and type_of_variable uri =
                 (NotWellTyped ("Variable " ^ (U.string_of_uri uri))))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        ty
    |  _ ->
        raise
@@ -529,10 +529,10 @@ and type_of_mutual_inductive_defs uri i =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -555,10 +555,10 @@ and type_of_mutual_inductive_constr uri i j =
    match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       Logger.log (`Start_type_checking uri) ;
+       CicLogger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       Logger.log (`Type_checking_completed uri) ;
+       CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -1762,7 +1762,7 @@ let typecheck uri =
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
-      Logger.log (`Start_type_checking uri) ;
+      CicLogger.log (`Start_type_checking uri) ;
       (match uobj with
           C.Constant (_,Some te,ty,_) ->
            let _ = type_of ty in
@@ -1802,5 +1802,5 @@ let typecheck uri =
            check_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      Logger.log (`Type_checking_completed uri)
+      CicLogger.log (`Type_checking_completed uri)
 ;;