]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicRefine.ml
removed debug prints
[helm.git] / helm / ocaml / cic_unification / cicRefine.ml
index 25af88f4feffb1b46ec477571b4848aab35fb7c1..98bafe9b89a0ac7f06db213e172ca84154f19a25 100644 (file)
@@ -523,12 +523,12 @@ and type_of_aux' metasenv context t ugraph =
                                       constructor_args_no
                                        (CicMetaSubst.apply_subst subst instance)
                                    in
-prerr_endline ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
+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
-prerr_endline ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
+debug_print ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst);
                                     candidate_oty,ugraph,metasenv,subst
 (* CSC: XXX
                                    let b,ugraph1 =