From c4844619c0fd9af77adee75ee218c726b48293e6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 10:02:57 +0000 Subject: [PATCH] Debugging print removed. --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2