removed no longer used METAs

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index f5527bec95898b925d5183e4c3d05745182f1544..f0d8ee46c7820b34feff186135edcd418b9b4fd4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 let debug = false ;;
@@ -51,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