diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/interface.mli | 2 | ||||
| -rw-r--r-- | lib/serialize.ml | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index a72e5b7b0f..52b5dbb7cb 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -15,6 +15,8 @@ type verbose = bool (** The type of coqtop goals *) type goal = { + goal_id : string; + (** Unique goal identifier *) goal_hyp : string list; (** List of hypotheses *) goal_ccl : string; diff --git a/lib/serialize.ml b/lib/serialize.ml index 3b43861314..a793e800eb 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -311,13 +311,15 @@ let to_evar = function let of_goal g = let hyp = of_list of_string g.goal_hyp in let ccl = of_string g.goal_ccl in - Element ("goal", [], [hyp; ccl]) + let id = of_string g.goal_id in + Element ("goal", [], [id; hyp; ccl]) let to_goal = function -| Element ("goal", [], [hyp; ccl]) -> +| Element ("goal", [], [id; hyp; ccl]) -> let hyp = to_list to_string hyp in let ccl = to_string ccl in - { goal_hyp = hyp; goal_ccl = ccl } + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | _ -> raise Marshal_error let of_goals g = |