Semantics of try changed (fixed) when applied to multiple goals that can now

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 0420c8119f2d6d9733e66e7799eb382e4ed874da..a9a46e7431dfe931b872edc4f4b8188ec68458b6 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -377,7 +377,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)