X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=f0d8ee46c7820b34feff186135edcd418b9b4fd4;hb=b1527286e32c8651d65619af61e3f638b3b89f8d;hp=f5527bec95898b925d5183e4c3d05745182f1544;hpb=93703370bfac25b4d342278388f54cc5e27cd531;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f5527bec9..f0d8ee46c 100644 --- 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