From e508aec3a90aca93c188c54b707d19114ef5ff83 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 6 Dec 2017 09:01:45 +0100 Subject: Proof engine: adding a function to save future goals including principal one. --- engine/evd.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'engine/evd.ml') diff --git a/engine/evd.ml b/engine/evd.ml index e0453713e..60bc2eb40 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -943,6 +943,8 @@ let future_goals evd = evd.future_goals let principal_future_goal evd = evd.principal_future_goal +let save_future_goals evd = (evd.future_goals, evd.principal_future_goal) + let reset_future_goals evd = { evd with future_goals = [] ; principal_future_goal=None } -- cgit v1.2.3