From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2008 10:02:57 +0000 (+0000)
Subject: Debugging print removed.
X-Git-Tag: make_still_working~5548
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4844619c0fd9af77adee75ee218c726b48293e6;p=helm.git

Debugging print removed.
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ff56df73e..fbb384d5e 100644
--- 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