fized disambiguation of LApply

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 16c3f0a481ad25d09233663ac1e15337666d26eb..5b5a76a7d0e6344fe0c1cdad993c9ce78b5bd696 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -440,9 +440,12 @@ let disambiguate_tactic status = function
      let status, to_what =
       match to_what with
          None -> status,None
-       | Some to_what -> status, Some (disambiguate_term status to_what) in
+       | Some to_what -> 
+           let status, to_what = disambiguate_term status to_what in
+           status, Some to_what
+     in
      let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, None, what)
+     status, TacticAst.LApply (loc, to_what, what)
   | TacticAst.Left loc -> status, TacticAst.Left loc
   | TacticAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in