Useless GrafiteTypes.get_baseuri removed.

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b1cc9d671f5acd17f0fcbf64931c4b220c3e7fd2..192e396af0f2838d0704a53226a9c41699504cf1 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -520,7 +520,7 @@ let eval_coercion status ~add_composites uri arity saturations =
  let status, lemmas =
   GrafiteSync.add_coercion ~add_composites 
     ~pack_coercion_obj:CicRefine.pack_coercion_obj
-   status uri arity saturations (GrafiteTypes.get_baseuri status) in
+   status uri arity saturations status#baseuri in
  let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
  let status = GrafiteTypes.add_moo_content [moo_content] status in 
   add_coercions_of_lemmas lemmas status
@@ -724,7 +724,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
      in
      let estatus,obj =
       GrafiteDisambiguate.disambiguate_nobj estatus
-       ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
+       ~baseuri:status#baseuri (text,prefix_len,obj) in
      let uri,height,nmenv,nsubst,nobj = obj in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
      let status =
@@ -792,7 +792,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      in
       res,`Old uris
   | GrafiteAst.Inverter (loc, name, indty, params) ->
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
      let indty_uri = 
        try CicUtil.uri_of_term indty
@@ -881,7 +881,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           ".ind",
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
      let obj = CicRefine.pack_coercion_obj obj in
      let metasenv = GrafiteTypes.get_proof_metasenv status in