]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/invokeTactics.ml
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / invokeTactics.ml
index cbe25219ce724b58c807c2aeae72cf2e62e0d9cc..13dc83f1d02dbba6531d18db4e70d5f0fdbc3321 100644 (file)
@@ -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