From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Jun 2005 13:03:49 +0000 (+0000)
Subject: Debugging code removed.
X-Git-Tag: PRE_INDEX_1~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c1967e287c35d226e773df8d221293c3c74c9d4;p=helm.git

Debugging code removed.
---

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 _