X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteEngine.ml;h=766408c13f5c25b4e3f3508f79fa1673d9b97cce;hb=5356519d50425dfca5b42ad5faeb2181d4240c78;hp=625b233233a559b723585dde7f41fda9ca810e2f;hpb=35a06fa8d6c2664301b59e77dcbff5bcfd4a5091;p=helm.git

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 625b23323..766408c13 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -38,7 +38,6 @@ type 'a disambiguator_input = string * int * 'a
 
 type options = { 
   do_heavy_checks: bool ; 
-  clean_baseuri: bool
 }
 
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
@@ -409,7 +408,6 @@ type eval_ast =
     Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
 
   ?do_heavy_checks:bool ->
-  ?clean_baseuri:bool ->
   GrafiteTypes.status ->
   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
   disambiguator_input ->
@@ -481,10 +479,10 @@ let refinement_toolkit = {
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
   
-let eval_coercion status ~add_composites uri arity saturations baseuri =
+let eval_coercion status ~add_composites uri arity saturations =
  let status,compounds =
   GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
-   saturations baseuri
+   saturations (GrafiteTypes.get_baseuri status)
  in
  let moo_content = 
    List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
@@ -569,7 +567,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
           with Not_found -> false,0            
         with Not_found -> assert false
       in
-      let buri, status = GrafiteTypes.get_baseuri status in
+      let buri = GrafiteTypes.get_baseuri status in
       (* looking at the fields we can know the 'wanted' coercions, but not the 
        * actually generated ones. So, only the intersection between the wanted
        * and the actual should be in the moo as coercion, while everithing in
@@ -648,8 +646,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,[] 
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
-     eval_coercion status ~add_composites uri arity saturations
-      (GrafiteTypes.get_string_option status "baseuri")
+     eval_coercion status ~add_composites uri arity saturations 
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
@@ -725,7 +722,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, status = GrafiteTypes.get_baseuri status in 
+     let buri = GrafiteTypes.get_baseuri status 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
@@ -830,13 +827,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        status)
     status moo
 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+~disambiguate_macro ?(do_heavy_checks=false) status
 (text,prefix_len,st)
 ->
-  let opts = {
-    do_heavy_checks = do_heavy_checks ; 
-    clean_baseuri = clean_baseuri }
-  in
+  let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
      eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command