Most warnings turned into errors and avoided

[helm.git] / matita / components / ng_kernel / nCicTypeChecker.ml

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index b60734508b46b5a6fe5687086ce7a8e45bfd640c..24217d6aea2628229ab3718dcf521ce267c4db4e 100644 (file)
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -1376,7 +1376,7 @@ let _ = NCicReduction.set_get_relevance get_relevance;;
 
 let indent = ref 0;;
 let debug = true;;
-let logger =
+let _logger =
     let do_indent () = String.make !indent ' ' in  
     (function 
       | `Start_type_checking s ->