From 4c45bc2cd4c610de0ac09c7e0897260fc253b684 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 27 Jun 2005 13:12:28 +0000
Subject: [PATCH] fized disambiguation of LApply

---
 helm/matita/matitaEngine.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

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
-- 
2.39.2