From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 27 Jun 2005 13:12:28 +0000 (+0000)
Subject: fized disambiguation of LApply
X-Git-Tag: INDEXING_NO_PROOFS~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c45bc2cd4c610de0ac09c7e0897260fc253b684;p=helm.git

fized disambiguation of LApply
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 16c3f0a48..5b5a76a7d 100644
--- 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