_metasenv <- [];
self#script#setGoal None
- method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+ method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
_metasenv <- metasenv;
pages <- 0;
let win goal_switch =
method private home () =
self#_showMath;
match self#script#grafite_status.proof_status with
- | Proof (uri, metasenv, bo, ty) ->
+ | Proof (uri, metasenv, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
- let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj
- | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+ | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
- let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj
| _ -> self#blank ()