Debugging code removed to achieve more tail-recursivity.

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