end
let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
+ LibraryClean.clean_baseuris [grafite_status#baseuri]
let save_moo grafite_status =
let script = MatitaScript.current () in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
let no_pstatus =
grafite_status#proof_status = GrafiteTypes.No_proof
in