"\n" ^
GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
- (GrafiteAst.Tactical (loc,
- GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
- Some (GrafiteAst.Semicolon loc))) in
+ (GrafiteAst.Tactic (loc,
+ Some (GrafiteAst.Reduce (loc, kind, pat)),
+ GrafiteAst.Semicolon loc)) in
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
_metasenv <- [];
self#script#setGoal None
- method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
+ method load_sequents
+ { proof = (_,metasenv,_subst,_,_, _) 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, attrs) ->
+ | Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj
- | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
+ | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj