match self#script#grafite_status.proof_status with
| Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
match self#script#grafite_status.proof_status with
| Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in