removed debug prerr_endline

[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 fe46e474849861fdfac7fa879d90e2322bcf7af3..74542a22696ce39cac7d3d9e81f63acf67a6817c 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -42,7 +42,7 @@ let debug t context =
    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
 ;;
 
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
 
 let rec split l n =
  match (l,n) with
@@ -184,7 +184,7 @@ let rec type_of_constant ~logger uri ugraph =
                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
         with Invalid_argument s ->
-          (*prerr_endline s;*)
+          (*debug_print s;*)
           uobj,ugraph_dust       
   in
    match cobj,ugraph with
@@ -225,7 +225,7 @@ and type_of_variable ~logger uri ugraph =
             | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
          with Invalid_argument s ->
-           (*prerr_endline s;*)
+           (*debug_print s;*)
            ty,ugraph2)
    |  _ ->
        raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
@@ -574,7 +574,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
             )
           with
               Invalid_argument s ->
-                (*prerr_endline s;*)
+                (*debug_print s;*)
                 uobj,ugraph1_dust
   in
     match cobj with
@@ -609,7 +609,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
                       raise CicEnvironmentError)
            with
                Invalid_argument s ->
-                 (*prerr_endline s;*)
+                 (*debug_print s;*)
                  uobj,ugraph1_dust
   in
     match cobj with
@@ -2037,12 +2037,12 @@ let typecheck uri ugraph =
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+       (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
        cobj,ugraph'
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+      (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
       let ugraph1 = 
        (match uobj with
          C.Constant (_,Some te,ty,_,_) ->
@@ -2111,7 +2111,7 @@ let typecheck uri ugraph =
              object.
            *)
            Invalid_argument s -> 
-             (*prerr_endline s;*)
+             (*debug_print s;*)
              uobj,ugraph1
 ;;