]> matita.cs.unibo.it Git - helm.git/commitdiff
Debugging print removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Mar 2008 10:02:57 +0000 (10:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Mar 2008 10:02:57 +0000 (10:02 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index ff56df73ec7d11f29acab1ddd1e09c49bfab1866..fbb384d5e66eb63909ae88aafaebb3a75f3c7c4e 100644 (file)
@@ -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