X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=13dc83f1d02dbba6531d18db4e70d5f0fdbc3321;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=cbe25219ce724b58c807c2aeae72cf2e62e0d9cc;hpb=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index cbe25219c..13dc83f1d 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -169,7 +169,7 @@ module Make (C: Callbacks) : Tactics =
       in
        handle_refresh_exception
         (fun () ->
-          let metasenv',expr =
+          let metasenv',expr,ugraph = (*TASSI:  FIX THIS*)
            (match term with
            | None -> ()
            | Some t -> (C.term_editor ())#set_term t);
@@ -235,7 +235,7 @@ module Make (C: Callbacks) : Tactics =
                     List.find (function (m,_,_) -> m=metano) metasenv
                    in
                     canonical_context in
-              let (metasenv',expr) =
+              let (metasenv',expr,ugraph) =(* FIX THIS AND *)
                (C.term_editor ())#get_metasenv_and_term
                 canonical_context metasenv
               in