let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
+ let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in
let reordered_metasenv, opened_goals =
reorder_metasenv
starting_metasenv
metasenv_after_refinement metasenv_after_tactic
opened goal always_opens_a_goal
in
- let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
+ let proof' = uri, reordered_metasenv, [], t, ty, attrs in
proof', opened_goals
in
let incomplete_proof =
NCicLibrary.add_obj uri obj;
{status with
GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status },`Old []
+ GrafiteTypes.CommandMode lexicon_status },`New [uri]
| _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
Setoids.add_relation id a aeq refl sym trans;
NCicLibrary.add_obj uri obj;
{status with
GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
- `Old []
+ `New [uri]
| _ ->
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
{ status with
GrafiteTypes.ProofMode
{ NTacStatus.gstatus = ninitial_stack;
istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
- },`Old [])
+ },`New [])
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
| GrafiteAst.NTactic (_(*loc*), tac, punct) ->
- (match status.GrafiteTypes.ng_status with
+ (match status.GrafiteTypes.ng_status with
| GrafiteTypes.CommandMode _ -> assert false
| GrafiteTypes.ProofMode nstatus ->
let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
NTacStatus.pp_tac_status nstatus;
- { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old [])
+ { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+ `New [])
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
eval_tactical status