Debugging code removed.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 98bafe9b89a0ac7f06db213e172ca84154f19a25..53dea97e9c43d2d820f61a96c9f37dff176698b9 100644 (file)
--- 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 _