diff options
| author | aspiwack | 2013-11-02 15:39:54 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:39:54 +0000 |
| commit | c9504af26647ab745dc22811a2db8058e0b66632 (patch) | |
| tree | 753c2029810002b23946636a3add74aacf86566c /lib/serialize.ml | |
| parent | 8d68ee674daa5deaa327b80e75f01876ef6ea9a0 (diff) | |
Adds a shelve tactic.
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/serialize.ml')
| -rw-r--r-- | lib/serialize.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index 88bf87c135..f3c06d9306 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -258,13 +258,15 @@ let of_goals g = let of_glist = of_list of_goal in let fg = of_list of_goal g.fg_goals in let bg = of_list (of_pair of_glist of_glist) g.bg_goals in - Element ("goals", [], [fg; bg]) + let shelf = of_list of_goal g.shelved_goals in + Element ("goals", [], [fg; bg; shelf]) let to_goals = function - | Element ("goals", [], [fg; bg]) -> + | Element ("goals", [], [fg; bg; shelf]) -> let to_glist = to_list to_goal in let fg = to_list to_goal fg in let bg = to_list (to_pair to_glist to_glist) bg in - { fg_goals = fg; bg_goals = bg; } + let shelf = to_list to_goal shelf in + { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; } | _ -> raise Marshal_error let of_coq_info info = |