From 2e729ae1dbbe53e34df5d2d5dc3122a6825be925 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 22 Nov 2010 21:49:57 +0000 Subject: [PATCH] Debugging code commented out. --- helm/software/components/ng_refiner/nCicRefineUtil.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 ;; -- 2.39.2