From cffe0bf6b541c6322e89ef6827d3e7d9f299bbe4 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 11 May 2012 15:28:49 +0000 Subject: Slightly modified the coqtop interface by adding an identifier in goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/serialize.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'lib/serialize.ml') diff --git a/lib/serialize.ml b/lib/serialize.ml index 3b4386131..a793e800e 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 = -- cgit v1.2.3