X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=83daf60a636309401e7637a9d2bdbc30caca9093;hb=ba2709d8c270e7f6ffbdb8bd3a192bc071407f03;hp=96b38e424970161afcbd301424eee55079f4adee;hpb=bf60fc57745fba8a2a22215ed1286eceae0f7700;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 96b38e424..83daf60a6 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -593,7 +593,7 @@ let delift n subst context metasenv l t =
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-print_endline "\nCicMetaSubst: UNCERTAIN" ;
+debug_print "\nCicMetaSubst: UNCERTAIN" ;
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)