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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a60e9e20d26c6bbe1b9a0bb65b0d4ca9056f6032..02f13739d5c14548e6da69f01a3c2c48e306d3e4 100644 (file)
--- 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