From e26fa4bf13639effcb838b971b11523cbd1aba2c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 May 2005 15:56:15 +0000 Subject: [PATCH] added intros n. --- helm/matita/matitaEngine.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -- 2.39.2