better manual generation

[helm.git] / helm / software / matita / matitaEngine.ml

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index fa9a0d393ab96ae7f3d879a0ba30caa478f2596c..d0e1c1acb989185c393ace5c27e9a9af8ffef7da 100644 (file)
--- 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