From 4c1967e287c35d226e773df8d221293c3c74c9d4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Jun 2005 13:03:49 +0000 Subject: [PATCH] Debugging code removed. --- helm/ocaml/cic_unification/cicRefine.ml | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 98bafe9b8..53dea97e9 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -523,23 +523,11 @@ and type_of_aux' metasenv context t ugraph = constructor_args_no (CicMetaSubst.apply_subst subst instance) in -debug_print ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst); let subst,metasenv,ugraph = fo_unif_subst subst context metasenv instance' ty ugraph in -debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst); candidate_oty,ugraph,metasenv,subst -(* CSC: XXX - let b,ugraph1 = - CicReduction.are_convertible context - instance' ty ugraph - in - if b then - candidate_oty,ugraph1,metasenv - else - None,ugraph,metasenv -*) with Failure _ | CicUnification.UnificationFailure _ -- 2.39.2