]> matita.cs.unibo.it Git - helm.git/commitdiff
removed prerr_endline.
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 20 May 2006 12:20:55 +0000 (12:20 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 20 May 2006 12:20:55 +0000 (12:20 +0000)
helm/software/components/tactics/paramodulation/saturation.ml

index 3bc8eb25bf2cfb13fce3641b6b40cf793d80ecc1..5eb62666f2d88ed5422a897f72d1e148fa01fc1b 100644 (file)
@@ -1311,7 +1311,6 @@ let infer_goal_set env active goals =
         let new' = Indexing.superposition_left env (snd active) selected in
         let metasenv, context, ugraph = env in
         let names = names_of_context context in
-        List.iter (fun (_,_,x) -> prerr_endline ("X: " ^ CicPp.pp x names)) new';
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in