X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefineUtil.ml;h=7015f1b5d11fe19695dcd26f11a39d34817165c4;hb=308d9394c3f8c0919427fcc7e00842e105840b4e;hp=745f571769c235f0d41357065851ad97c75bfc98;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_refiner/nCicRefineUtil.ml b/matita/components/ng_refiner/nCicRefineUtil.ml
index 745f57176..7015f1b5d 100644
--- a/matita/components/ng_refiner/nCicRefineUtil.ml
+++ b/matita/components/ng_refiner/nCicRefineUtil.ml
@@ -128,12 +128,14 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
        NCic.Match (it,substaux k ctx what outt, substaux k ctx what t,
         List.map (substaux k ctx what) pl)
  in
+(*
   prerr_endline "*** replace lifting -- what:";
   List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what;
   prerr_endline "\n*** replace lifting -- with what:";
   List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what;
   prerr_endline "\n*** replace lifting -- where:";
   prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where);
+*)
 
   substaux 1 context what where
 ;;