Just code clean-up.

[helm.git] / helm / ocaml / cic_proof_checking / cicReduction.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index e0ad91f59b2414c3c855fb07287edc0f0e341c88..395d7a69693340fa037124c810e5cd3648b11b2f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -202,7 +202,7 @@ 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" );*)
+let res =
       match (t1',t2') with
          (C.Rel n1, C.Rel n2) -> n1 = n2
        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
@@ -262,6 +262,8 @@ let are_convertible t1 t2 =
        | (_,_) ->
           debug t1' [t2'] "NOT-CONVERTIBLE" ;
           false
+in
+if res then true else (debug t1' [t2'] "NOT-CONVERTIBLE" ; false)
    end
  in
   aux t1 t2