Debugging code commented out.

diff --git a/helm/software/components/ng_refiner/nCicRefineUtil.ml b/helm/software/components/ng_refiner/nCicRefineUtil.ml
index 745f571769c235f0d41357065851ad97c75bfc98..4f7277f9e6e6f6ba2c205dc39cf63b09f8d8eef9 100644 (file)
--- 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
 ;;