X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=e55df286b87b5a0d6f069bb4f7de9228cc3f00e4;hb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;hp=e8abb057295acf3a49dedc8e0b7df19e28fc1e2e;hpb=a3417bd94b857a7f96a2221ba5b79444823b2144;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e8abb0572..e55df286b 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -808,6 +808,7 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
   | GrafiteAst.NInversion (_loc, what, where) ->
       NTactics.inversion_tac 
         ~what:(text,prefix_len,what)