From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 30 May 2005 15:56:15 +0000 (+0000)
Subject: added intros n.
X-Git-Tag: PRE_INDEX_1~105
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e26fa4bf13639effcb838b971b11523cbd1aba2c;p=helm.git

added intros n.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 89949cd1d..990276878 100644
--- 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