X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=f0d8ee46c7820b34feff186135edcd418b9b4fd4;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=6fca24b13d96b829476f3773d712db036d73b170;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 6fca24b13..f0d8ee46c 100644
--- 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