diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35ca18e4f5..b8886b9b54 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1007,6 +1007,9 @@ let principal_future_goal evd = evd.principal_future_goal let reset_future_goals evd = { evd with future_goals = [] ; principal_future_goal=None } +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } + let meta_diff ext orig = Metamap.fold (fun m v acc -> if Metamap.mem m orig then acc |