]> matita.cs.unibo.it Git - helm.git/commitdiff
removed debug prints
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:44:27 +0000 (11:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:44:27 +0000 (11:44 +0000)
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 =