added intros n.

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 89949cd1db8099e724f0ba77bb08da13830eb03e..990276878ab5fde8cff61231196c1cb764e068f9 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -19,9 +19,12 @@ let namer_of names =
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
 let tactic_of_ast = function
-  | TacticAst.Intros (_, _, names) ->
+  | TacticAst.Intros (_, None, names) ->
       (* TODO Zack implement intros length *)
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+  | TacticAst.Intros (_, Some num, names) ->
+      (* TODO Zack implement intros length *)
+      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction