- bug fixed (introduced by last commit from Andrea in MatitaEngine):

[helm.git] / matita / components / ng_refiner / nCicRefineUtil.ml

diff --git a/matita/components/ng_refiner/nCicRefineUtil.ml b/matita/components/ng_refiner/nCicRefineUtil.ml
index 745f571769c235f0d41357065851ad97c75bfc98..7015f1b5d11fe19695dcd26f11a39d34817165c4 100644 (file)
--- 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
 ;;