X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaEngine.ml;h=d0e1c1acb989185c393ace5c27e9a9af8ffef7da;hb=a3d01f7170dd84f90481d53e271580e10e46ae75;hp=fa9a0d393ab96ae7f3d879a0ba30caa478f2596c;hpb=ed89063fccf02a7a63cae52292e3ff0cc2548731;p=helm.git

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index fa9a0d393..d0e1c1acb 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -35,7 +35,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t
   GrafiteDisambiguate.disambiguate_tactic
    lexicon_status_ref
    (GrafiteTypes.get_proof_context grafite_status goal)
-   (GrafiteTypes.get_proof_metasenv grafite_status)
+   (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal)
    tac
  in
   GrafiteTypes.set_metasenv metasenv grafite_status,tac