let pp_ast_statement grafite_status stm =
let stm = GrafiteAstPp.pp_statement
~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
- ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj
- CicNotationPp.pp_term) stm
+ ~term_pp:NotationPp.pp_term
+ ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj
+ NotationPp.pp_term) stm
in
let stm = Pcre.replace ~rex:slash_n_RE stm in
let stm =
let floc = H.dummy_floc in
let nl_ast = G.Comment (floc, G.Note (floc, "")) in
let pp_statement stm =
- GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- ~lazy_term_pp:CicNotationPp.pp_term
- ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
+ ~lazy_term_pp:NotationPp.pp_term
+ ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
in
let pp_lexicon = LexiconAstPp.pp_command in
let och = open_out f in
;;
let activate_extraction baseuri fname =
+ ()
+ (* MATITA 1.0
if Helm_registry.get_bool "matita.extract" then
let mangled_baseuri =
let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
(fun ~add_obj ~add_coercion _ obj ->
output_string f (CicExportation.ppobj baseuri obj);
flush f; []);
+ *)
;;
let compile atstart options fname =