blob: db5c733d3a98b811fe33c4ab288054933bf24cfb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Utility for applying tactic and incorproating results into goal tree. *)
(* Takes an "infotactic", i.e. like a normal tactic that works on 'goal' and *)
(* returns 'goalstate', but that also returns 'finfo' which summarises the *)
(* operation. These are easily formed by tagging normal tactics. *)
let infotactic_wrap0 (infotac:goal->(goalstate*finfo)) (gx:xgoal) : xgoalstate =
let (g,id) = dest_xgoal gx in
let ((meta,gs,just),gst) = infotac g in
let gxs = extend_gtree id gst gs in
(meta,gxs,just);;
|
