From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 Dec 2001 11:57:06 +0000 (+0000)
Subject: Debugging code removed to achieve more tail-recursivity.
X-Git-Tag: mlminidom_0_2_2~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39b862c075fad2536c35ed3515a0b1ffd478681a;p=helm.git

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 395d7a696..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";
-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