new intro:

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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e8abb057295acf3a49dedc8e0b7df19e28fc1e2e..e55df286b87b5a0d6f069bb4f7de9228cc3f00e4 100644 (file)
--- 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)