From 39b862c075fad2536c35ed3515a0b1ffd478681a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 5 Dec 2001 11:57:06 +0000 Subject: [PATCH] Debugging code removed to achieve more tail-recursivity. --- helm/ocaml/cic_proof_checking/cicReduction.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) 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 -- 2.39.2