- ApplyTransformation.txt_of_cic_sequent_conclusion
+ let map_unicode_to_tex =
+ Helm_registry.get_opt Helm_registry.bool "matita.paste_unicode_as_tex" in
+ ApplyTransformation.txt_of_cic_sequent_conclusion ?map_unicode_to_tex
- method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+ method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
let str = CoercGraph.generate_dot_file () in
let filename, oc = Filename.open_temp_file "matita" ".dot" in
output_string oc str;
close_out oc;
let str = CoercGraph.generate_dot_file () in
let filename, oc = Filename.open_temp_file "matita" ".dot" in
output_string oc str;
close_out oc;
method private _load ?(force=false) entry =
handle_error (fun () ->
if entry <> current_entry || entry = `About `Current_proof || entry =
method private _load ?(force=false) entry =
handle_error (fun () ->
if entry <> current_entry || entry = `About `Current_proof || entry =
begin
(match entry with
| `About `Current_proof -> self#home ()
| `About `Blank -> self#blank ()
| `About `Us -> self#egg ()
begin
(match entry with
| `About `Current_proof -> self#home ()
| `About `Blank -> self#blank ()
| `About `Us -> self#egg ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Development d -> self#_showDevelDeps d
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Development d -> self#_showDevelDeps d
- | Proof (uri, metasenv, bo, ty) ->
+ | Proof (uri, metasenv, bo, ty, attrs) ->
- let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
- | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+ | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
- let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in