From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Jun 2005 09:16:54 +0000 (+0000)
Subject: New argument for LApply: the ident for the generated hypothesis.
X-Git-Tag: INDEXING_NO_PROOFS~29
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a9d597352e104434a1a7f371fdd1bbdac5e50a3;p=helm.git

New argument for LApply: the ident for the generated hypothesis.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a60e9e20d..02f13739d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -67,8 +67,9 @@ let tactic_of_ast = function
   | TacticAst.Intros (_, Some num, names) ->
       PrimitiveTactics.intros_tac ~howmany:num
         ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.LApply (_, to_what, what) ->
-     Tactics.lapply ?to_what what
+  | TacticAst.LApply (_, to_what, what, ident) ->
+     let names = match ident with None -> [] | Some id -> [id] in
+     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -449,7 +450,7 @@ let disambiguate_tactic status = function
       status, TacticAst.Injection (loc,term)
   | TacticAst.Intros (loc, num, names) ->
       status, TacticAst.Intros (loc, num, names)
-  | TacticAst.LApply (loc, to_what, what) ->
+  | TacticAst.LApply (loc, to_what, what, ident) ->
      let status, to_what =
       match to_what with
          None -> status,None
@@ -458,7 +459,7 @@ let disambiguate_tactic status = function
            status, Some to_what
      in
      let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, to_what, what)
+     status, TacticAst.LApply (loc, to_what, what, ident)
   | TacticAst.Left loc -> status, TacticAst.Left loc
   | TacticAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in