X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ca02263b01e6de6aceeff38012aa5e98be2e573a;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=976b25b55a79f8e7c6f3659777481b1ccaa9a4de;hpb=8156d113837e31604dd91340f58c4dc8c155503a;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 976b25b55..ca02263b0 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -831,7 +831,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (aux f (text, prefix_len, tac))
+      (f f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
   | GrafiteAst.NBlock (_,l) -> 
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
@@ -888,7 +888,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-        prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
+        (*prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);*)
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =