Debugging print removed.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ff56df73ec7d11f29acab1ddd1e09c49bfab1866..fbb384d5e66eb63909ae88aafaebb3a75f3c7c4e 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1519,8 +1519,8 @@ and check_metasenv_consistency ~logger ~subst metasenv context
                  Failure _ -> t)
             | _ -> t
           in
-if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
-else prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);
+(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
+else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
           let b,ugraph1 = 
             R.are_convertible ~subst ~metasenv context optimized_t ct ugraph 
           in