From: Claudio Sacerdoti Coen 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