diff options
| -rw-r--r-- | hol-light/TacticRecording/graveyard.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/hol-light/TacticRecording/graveyard.ml b/hol-light/TacticRecording/graveyard.ml deleted file mode 100644 index db5c733d..00000000 --- a/hol-light/TacticRecording/graveyard.ml +++ /dev/null @@ -1,12 +0,0 @@ - - -(* 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);; |