Bug fixed: macros in the middle of a goto cursor or goto end-of-script were

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 6fca24b13d96b829476f3773d712db036d73b170..f0d8ee46c7820b34feff186135edcd418b9b4fd4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -53,13 +53,12 @@ let disambiguate_command lexicon_status_ref grafite_status cmd =
   lexicon_status_ref := lexicon_status;
   GrafiteTypes.set_metasenv metasenv grafite_status,cmd
 
-let disambiguate_macro lexicon_status_ref grafite_status macro goal =
+let disambiguate_macro lexicon_status_ref grafite_status macro context =
  let metasenv,macro =
   GrafiteDisambiguate.disambiguate_macro
    lexicon_status_ref
    (GrafiteTypes.get_proof_metasenv grafite_status)
-   (GrafiteTypes.get_proof_context grafite_status goal)
-   macro
+   context macro
  in
   GrafiteTypes.set_metasenv metasenv grafite_status,macro