Useless GrafiteTypes.get_baseuri removed.

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

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 6b16891c883621460ccfb5c7133eebd4aa465067..ba4e346969a2757af26c63c9a979f8097b3d77ac 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -41,7 +41,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t
   GrafiteTypes.set_metasenv metasenv grafite_status,tac
 
 let disambiguate_command lexicon_status_ref grafite_status cmd =
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
  let lexicon_status,metasenv,cmd =
   GrafiteDisambiguate.disambiguate_command ~baseuri
    !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
@@ -62,7 +62,7 @@ let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) =
  let lexicon_status = GrafiteTypes.get_estatus grafite_status in
  let dump = not (Helm_registry.get_bool "matita.moo") in
  let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
  let new_grafite_status,new_objs =
   match ast with 
      | G.Executable (_, G.Command (_, G.Coercion _)) when dump ->