X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefineUtil.ml;h=4f7277f9e6e6f6ba2c205dc39cf63b09f8d8eef9;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hp=745f571769c235f0d41357065851ad97c75bfc98;hpb=e62111335574a6ec78e5a4367a540e0529a00404;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefineUtil.ml b/helm/software/components/ng_refiner/nCicRefineUtil.ml
index 745f57176..4f7277f9e 100644
--- a/helm/software/components/ng_refiner/nCicRefineUtil.ml
+++ b/helm/software/components/ng_refiner/nCicRefineUtil.ml
@@ -128,12 +128,12 @@ 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:";
+  (*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);
+  prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where);*)
 
   substaux 1 context what where
 ;;