let script = MatitaScript.current () in
let baseuri = GrafiteTypes.get_baseuri grafite_status in
let no_pstatus =
- grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+ grafite_status#proof_status = GrafiteTypes.No_proof
in
match script#bos, script#eos, no_pstatus with
| true, _, _ -> ()
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname
- grafite_status.GrafiteTypes.moo_content_rev;
+ GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
(GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev;
NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)