type options = {
do_heavy_checks: bool ;
- clean_baseuri: bool
}
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
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 ->
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)
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
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,[]
".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
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