diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-11 15:28:49 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-11 15:28:49 +0000 |
| commit | cffe0bf6b541c6322e89ef6827d3e7d9f299bbe4 (patch) | |
| tree | a84fe194f15a086ad691e877181872d21a61d27b /lib/serialize.ml | |
| parent | 5ea279dbd47d9ef1b87351e4df469aba3310f3f0 (diff) | |
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
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 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 = |