X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=ac1b50d31afd8340b82c188b64ad54a8ce62fecd;hb=10434de696a721d9ea1b4eddc4169d601ee671e5;hp=e0ad91f59b2414c3c855fb07287edc0f0e341c88;hpb=ae326f646ef4c01b43d6da04201b427d1e175400;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index e0ad91f59..ac1b50d31 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -202,7 +202,6 @@ let are_convertible t1 t2 =
      let t1' = whd t1 
      and t2' = whd t2 in
      debug t1' [t2'] "POSTWHD";
-     (*if !fdebug = 0 then ignore(Unix.system "read" );*)
       match (t1',t2') with
          (C.Rel n1, C.Rel n2) -> n1 = n2
        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
@@ -259,9 +258,7 @@ let are_convertible t1 t2 =
        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
        | (C.Implicit, _) | (_, C.Implicit) ->
           raise (Impossible 3) (* we don't trust our whd ;-) *)
-       | (_,_) ->
-          debug t1' [t2'] "NOT-CONVERTIBLE" ;
-          false
+       | (_,_) -> false
    end
  in
   aux t1 t2