- ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)
- in
- let status,goals = tactical_of_ast tac status in
- let proof,_ = MatitaMisc.get_proof_status status in
- let new_status =
- match goals with
- | [] ->
- let (_,metasenv,_,_) = proof in
- (match metasenv with
- | [] -> Proof proof
- | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
- | ng::_ -> Incomplete_proof (proof, ng)
+ ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
+
+ | GrafiteAst.Skip loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ in
+ let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
+ let status = (* is proof completed? *)
+ match status.proof_status with
+ | Incomplete_proof { stack = stack; proof = proof }
+ when Continuationals.Stack.is_empty stack ->
+ { status with proof_status = Proof proof }
+ | _ -> status