let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| Incomplete_proof ((uri, metasenv, bo, ty), _) ->
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
self#_loadObj obj
| Incomplete_proof ((uri, metasenv, bo, ty), _) ->